iend = n.end();
i != iend; ) {
out << '(';
- (*i).toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
- types, language::output::LANG_SMTLIB_V2);
+ toStream(out, (*i), toDepth < 0 ? toDepth : toDepth - 1, types);
out << ' ';
out << (*i).getType();
// The following code do stange things
option repeatSimp --repeat-simp bool :read-write
make multiple passes with nonclausal simplifier
+option sortInference --sort-inference bool :default false
+ apply sort inference to input problem
+
common-option incrementalSolving incremental -i --incremental bool
enable incremental solving
#include "printer/printer.h"
#include "prop/options.h"
#include "theory/arrays/options.h"
+#include "util/sort_inference.h"
using namespace std;
using namespace CVC4;
if (options::checkModels()) {
Warning() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << std::endl;
setOption("check-models", SExpr("false"));
- }
+ }
}
}
}else{
TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, n[0][i].getType() );
Node op = NodeManager::currentNM()->mkSkolem( "skop_$$", typ, "op created during pre-skolemization" );
+ //DOTHIS: set attribute on op, marking that it should not be selected as trigger
std::vector< Node > funcArgs;
funcArgs.push_back( op );
funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() );
}
dumpAssertions("post-skolem-quant", d_assertionsToPreprocess);
+ if( options::sortInference() ){
+ //sort inference technique
+ //TODO: use this as a rewrite technique here?
+ SortInference si;
+ si.simplify( d_assertionsToPreprocess );
+ }
+
dumpAssertions("pre-simplify", d_assertionsToPreprocess);
Chat() << "simplifying assertions..." << endl;
bool noConflict = simplifyAssertions();
d_cg = new CandidateGeneratorQueue;\r
if( !Trigger::getPatternArithmetic( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){\r
Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;\r
- Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;\r
+ //Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;\r
d_matchPolicy = MATCH_GEN_INTERNAL_ERROR;\r
}else{\r
Debug("matching-arith") << "Generated arithmetic pattern for " << d_match_pattern << ": " << std::endl;\r
int addedLemmas = 0;
FirstOrderModel* fm = d_quantEngine->getModel();
//for debugging
- if( Trace.isOn("model-engine") ){
+ if( Trace.isOn("model-engine") || Trace.isOn("model-engine-debug") ){
for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
it != fm->d_rep_set.d_type_reps.end(); ++it ){
if( it->first.isSort() ){
d_testLemmas = 0;
d_relevantLemmas = 0;
d_totalLemmas = 0;
- Debug("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
+ Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node f = fm->getAssertedQuantifier( i );
//keep track of total instantiations for statistics
//create a rep set iterator and iterate over the (relevant) domain of the quantifier
RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) );
- riter.setQuantifier( f );
- //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
- d_incomplete_check = d_incomplete_check || riter.d_incomplete;
- //set the domain for the iterator (the sufficient set of instantiations to try)
- if( useRelInstDomain ){
- riter.setDomain( d_rel_domain.d_quant_inst_domain[f] );
- }
- d_quantEngine->getModel()->resetEvaluate();
- int tests = 0;
- int triedLemmas = 0;
- while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){
- d_testLemmas++;
- int eval = 0;
- int depIndex;
- if( d_builder->optUseModel() ){
- //see if instantiation is already true in current model
- Debug("fmf-model-eval") << "Evaluating ";
- riter.debugPrintSmall("fmf-model-eval");
- Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
- tests++;
- //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 );
- if( eval==1 ){
- Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl;
- }else{
- Debug("fmf-model-eval") << " Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl;
- }
+ if( riter.setQuantifier( f ) ){
+ //set the domain for the iterator (the sufficient set of instantiations to try)
+ if( useRelInstDomain ){
+ riter.setDomain( d_rel_domain.d_quant_inst_domain[f] );
}
- if( eval==1 ){
- //instantiation is already true -> skip
- riter.increment2( depIndex );
- }else{
- //instantiation was not shown to be true, construct the match
- InstMatch m;
- for( int i=0; i<riter.getNumTerms(); i++ ){
- m.set( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, riter.d_index_order[i] ), riter.getTerm( i ) );
+ d_quantEngine->getModel()->resetEvaluate();
+ int tests = 0;
+ int triedLemmas = 0;
+ while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){
+ d_testLemmas++;
+ int eval = 0;
+ int depIndex;
+ if( d_builder->optUseModel() ){
+ //see if instantiation is already true in current model
+ Debug("fmf-model-eval") << "Evaluating ";
+ riter.debugPrintSmall("fmf-model-eval");
+ Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
+ tests++;
+ //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 );
+ if( eval==1 ){
+ Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl;
+ }else{
+ Debug("fmf-model-eval") << " Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl;
+ }
}
- Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
- triedLemmas++;
- d_triedLemmas++;
- //add as instantiation
- if( d_quantEngine->addInstantiation( f, m ) ){
- addedLemmas++;
- //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
- if( eval==-1 && optExhInstEvalSkipMultiple() ){
- riter.increment2( depIndex );
+ if( eval==1 ){
+ //instantiation is already true -> skip
+ riter.increment2( depIndex );
+ }else{
+ //instantiation was not shown to be true, construct the match
+ InstMatch m;
+ for( int i=0; i<riter.getNumTerms(); i++ ){
+ m.set( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, riter.d_index_order[i] ), riter.getTerm( i ) );
+ }
+ Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
+ triedLemmas++;
+ d_triedLemmas++;
+ //add as instantiation
+ if( d_quantEngine->addInstantiation( f, m ) ){
+ addedLemmas++;
+ //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
+ if( eval==-1 && optExhInstEvalSkipMultiple() ){
+ riter.increment2( depIndex );
+ }else{
+ riter.increment();
+ }
}else{
+ Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
riter.increment();
}
- }else{
- Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
- riter.increment();
}
}
+ //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;
+ int relevantInst = 1;
+ for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+ relevantInst = relevantInst * (int)riter.d_domain[i].size();
+ }
+ d_relevantLemmas += relevantInst;
+ Debug("inst-fmf-ei") << "Finished: " << std::endl;
+ //Debug("inst-fmf-ei") << " Inst Total: " << totalInst << std::endl;
+ Debug("inst-fmf-ei") << " Inst Relevant: " << relevantInst << std::endl;
+ Debug("inst-fmf-ei") << " Inst Tried: " << triedLemmas << std::endl;
+ Debug("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl;
+ Debug("inst-fmf-ei") << " # Tests: " << tests << std::endl;
+ if( addedLemmas>1000 ){
+ Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl;
+ //Trace("model-engine-warn") << " Inst Total: " << totalInst << std::endl;
+ Trace("model-engine-warn") << " Inst Relevant: " << relevantInst << std::endl;
+ Trace("model-engine-warn") << " Inst Tried: " << triedLemmas << std::endl;
+ Trace("model-engine-warn") << " Inst Added: " << addedLemmas << std::endl;
+ Trace("model-engine-warn") << " # Tests: " << tests << std::endl;
+ Trace("model-engine-warn") << std::endl;
+ }
}
- //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;
- int relevantInst = 1;
- for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- relevantInst = relevantInst * (int)riter.d_domain[i].size();
- }
- d_relevantLemmas += relevantInst;
- Debug("inst-fmf-ei") << "Finished: " << std::endl;
- //Debug("inst-fmf-ei") << " Inst Total: " << totalInst << std::endl;
- Debug("inst-fmf-ei") << " Inst Relevant: " << relevantInst << std::endl;
- Debug("inst-fmf-ei") << " Inst Tried: " << triedLemmas << std::endl;
- Debug("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl;
- Debug("inst-fmf-ei") << " # Tests: " << tests << std::endl;
- if( addedLemmas>1000 ){
- Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl;
- //Trace("model-engine-warn") << " Inst Total: " << totalInst << std::endl;
- Trace("model-engine-warn") << " Inst Relevant: " << relevantInst << std::endl;
- Trace("model-engine-warn") << " Inst Tried: " << triedLemmas << std::endl;
- Trace("model-engine-warn") << " Inst Added: " << addedLemmas << std::endl;
- Trace("model-engine-warn") << " # Tests: " << tests << std::endl;
- Trace("model-engine-warn") << std::endl;
- }
+ //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
+ d_incomplete_check = d_incomplete_check || riter.d_incomplete;
return addedLemmas;
}
option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h"
policy for instantiating axioms
+
endmodule
return true;
}else if( n.getKind()==MULT ){
if( n[0].getKind()==INST_CONSTANT && n[0].getAttribute(InstConstantAttribute())==f ){
- Assert( !n[1].hasAttribute(InstConstantAttribute()) );
- coeffs[ n[0] ] = n[1];
- return true;
+ if( !n[1].hasAttribute(InstConstantAttribute()) ){
+ coeffs[ n[0] ] = n[1];
+ return true;
+ }
}else if( n[1].getKind()==INST_CONSTANT && n[1].getAttribute(InstConstantAttribute())==f ){
- Assert( !n[0].hasAttribute(InstConstantAttribute()) );
- coeffs[ n[1] ] = n[0];
- return true;
+ if( !n[0].hasAttribute(InstConstantAttribute()) ){
+ coeffs[ n[1] ] = n[0];
+ return true;
+ }
}
}
return false;
\r
}\r
\r
-void RepSetIterator::setQuantifier( Node f ){\r
+bool RepSetIterator::setQuantifier( Node f ){\r
Assert( d_types.empty() );\r
//store indicies\r
for( size_t i=0; i<f[0].getNumChildren(); i++ ){\r
d_types.push_back( f[0][i].getType() );\r
}\r
- initialize();\r
+ return initialize();\r
}\r
\r
-void RepSetIterator::setFunctionDomain( Node op ){\r
+bool RepSetIterator::setFunctionDomain( Node op ){\r
Assert( d_types.empty() );\r
TypeNode tn = op.getType();\r
for( size_t i=0; i<tn.getNumChildren()-1; i++ ){\r
d_types.push_back( tn[i] );\r
}\r
- initialize();\r
+ return initialize();\r
}\r
\r
-void RepSetIterator::initialize(){\r
+bool RepSetIterator::initialize(){\r
for( size_t i=0; i<d_types.size(); i++ ){\r
d_index.push_back( 0 );\r
//store default index order\r
d_incomplete = true;\r
}\r
}else{\r
- Trace("fmf-incomplete") << "Incomplete because of type " << tn << std::endl;\r
+ Trace("fmf-incomplete") << "Incomplete because of unknown type " << tn << std::endl;\r
d_incomplete = true;\r
}\r
if( d_rep_set->hasType( tn ) ){\r
d_domain[i].push_back( j );\r
}\r
}else{\r
- Trace("fmf-incomplete") << "Incomplete, unknown type " << tn << std::endl;\r
- d_incomplete = true;\r
- Unimplemented("Cannot create representative set iterator for unknown type quantifier");\r
+ return false;\r
}\r
}\r
+ return true;\r
}\r
\r
void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){\r
class RepSetIterator {\r
private:\r
//initialize function\r
- void initialize();\r
+ bool initialize();\r
public:\r
RepSetIterator( RepSet* rs );\r
~RepSetIterator(){}\r
//set that this iterator will be iterating over instantiations for a quantifier\r
- void setQuantifier( Node f );\r
+ bool setQuantifier( Node f );\r
//set that this iterator will be iterating over the domain of a function\r
- void setFunctionDomain( Node op );\r
+ bool setFunctionDomain( Node op );\r
public:\r
//pointer to model\r
RepSet* d_rep_set;\r
option ufssColoringSat --uf-ss-coloring-sat bool :default false
use coloring-based SAT heuristic for uf strong solver
option ufssTotality --uf-ss-totality bool :default false
- use totality axioms for enforcing cardinality constraints
+ always use totality axioms for enforcing cardinality constraints
+option ufssTotalityLimited --uf-ss-totality-limited=N int :default -1
+ apply totality axioms, but only up to cardinality N (-1 == do not apply totality axioms, default)
option ufssTotalityLazy --uf-ss-totality-lazy bool :default false
apply totality axioms lazily
option ufssAbortCardinality --uf-ss-abort-card=N int :default -1
tells the uf strong solver a cardinality to abort at (-1 == no limit, default)
option ufssSmartSplits --uf-ss-smart-split bool :default false
use smart splitting heuristic for uf strong solver
-option ufssModelInference --uf-ss-model-infer bool :default false
- use model inference method for uf strong solver
option ufssExplainedCliques --uf-ss-explained-cliques bool :default false
add explained clique lemmas for uf strong solver
}
return;
}else{
- if( applyTotality( d_cardinality ) ){
- //if we are applying totality to this cardinality
- if( options::ufssTotalityLazy() ){
- //add totality axioms for all nodes that have not yet been equated to cardinality terms
- if( level==Theory::EFFORT_FULL ){
- for( NodeIntMap::iterator it = d_regions_map.begin(); it != d_regions_map.end(); ++it ){
- if( !options::ufssTotality() || d_regions_map[ (*it).first ]!=-1 ){
- addTotalityAxiom( (*it).first, d_cardinality, &d_th->getOutputChannel() );
- }
- }
- }
- }
- }else{
+ //first check if we can generate a clique conflict
+ if( !options::ufssTotality() ){
//do a check within each region
for( int i=0; i<(int)d_regions_index; i++ ){
if( d_regions[i]->d_valid ){
}
}
}
- bool addedLemma = false;
+ }
+ if( applyTotality( d_cardinality ) ){
+ //add totality axioms for all nodes that have not yet been equated to cardinality terms
+ if( options::ufssTotalityLazy() ){ //this should always be true
+ if( level==Theory::EFFORT_FULL ){
+ for( NodeIntMap::iterator it = d_regions_map.begin(); it != d_regions_map.end(); ++it ){
+ if( !options::ufssTotality() || d_regions_map[ (*it).first ]!=-1 ){
+ addTotalityAxiom( (*it).first, d_cardinality, &d_th->getOutputChannel() );
+ }
+ }
+ }
+ }
+ }else{
//do splitting on demand
+ bool addedLemma = false;
if( level==Theory::EFFORT_FULL || options::ufssEagerSplits() ){
Trace("uf-ss-debug") << "Add splits?" << std::endl;
//see if we have any recommended splits from large regions
}
}
}else{
+ /*
if( options::ufssModelInference() ){
//check if we are at decision level 0
if( d_th->d_valuation.getAssertionLevel()==0 ){
}
}
}
+ */
//see if we need to request a new cardinality
if( !d_hasCard ){
bool needsCard = true;
Message() << "Maximum cardinality reached." << std::endl;
exit( 0 );
}else{
- if( options::ufssTotality() ){
+ if( applyTotality( d_aloc_cardinality ) ){
//must generate new cardinality lemma term
- std::stringstream ss;
- ss << "_c_" << d_aloc_cardinality;
Node var;
- if( d_totality_terms[0].empty() ){
+ if( d_aloc_cardinality==1 ){
//get arbitrary ground term
var = d_cardinality_term;
}else{
+ std::stringstream ss;
+ ss << "_c_" << d_aloc_cardinality;
var = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "is a cardinality lemma term" );
}
d_totality_terms[0].push_back( var );
out->lemma( lem );
return;
}
- if( options::ufssModelInference() || Trace.isOn("uf-ss-cliques") ){
+ //if( options::ufssModelInference() ||
+ if( Trace.isOn("uf-ss-cliques") ){
std::vector< Node > clique_vec;
clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() );
d_cliques[ d_cardinality ].push_back( clique_vec );
/** apply totality */
bool StrongSolverTheoryUf::SortRepModel::applyTotality( int cardinality ){
- return options::ufssTotality() || ( options::ufssModelInference() && !d_totality_terms[cardinality].empty() );
+ return options::ufssTotality() || cardinality<=options::ufssTotalityLimited();
+ // || ( options::ufssModelInference() && !d_totality_terms[cardinality].empty() );
}
/** get totality lemma terms */
Node StrongSolverTheoryUf::SortRepModel::getTotalityLemmaTerm( int cardinality, int i ){
- if( options::ufssTotality() ){
- return d_totality_terms[0][i];
- }else{
- return d_totality_terms[cardinality][i];
- }
+ return d_totality_terms[0][i];
+ //}else{
+ // return d_totality_terms[cardinality][i];
+ //}
}
void StrongSolverTheoryUf::SortRepModel::debugPrint( const char* c ){
}
void StrongSolverTheoryUf::preRegisterTerm( TNode n ){
+ Trace("uf-ss-register") << "Preregister " << n << "." << std::endl;
//shouldn't have to preregister this type (it may be that there are no quantifiers over tn)
TypeNode tn = n.getType();
if( d_rep_model.find( tn )==d_rep_model.end() ){
RepModel* rm = NULL;
if( tn.isSort() ){
- Debug("uf-ss-register") << "Preregister sort " << tn << "." << std::endl;
+ Trace("uf-ss-register") << "Preregister sort " << tn << "." << std::endl;
rm = new SortRepModel( n, d_th->getSatContext(), d_th );
}else if( tn.isInteger() ){
//rm = new InfRepModel( tn, d_th->getSatContext(), d_th );
d_rep_model[tn] = rm;
d_rep_model_init[tn] = true;
}
+ }else{
+ Trace("uf-ss-register") << "Already preregistered sort " << tn << "." << std::endl;
}
}
array_store_all.h \
array_store_all.cpp \
util_model.h \
- util_model.cpp
+ util_model.cpp \
+ sort_inference.h \
+ sort_inference.cpp
libutil_la_LIBADD = \
@builddir@/libutilcudd.la
--- /dev/null
+/********************* */\r
+/*! \file sort_inference.cpp\r
+ ** \verbatim\r
+ ** Original author: ajreynol\r
+ ** Major contributors: none\r
+ ** Minor contributors (to current version): none\r
+ ** This file is part of the CVC4 prototype.\r
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief Sort inference module\r
+ **\r
+ ** This class implements sort inference, based on a simple algorithm:\r
+ ** First, we assume all functions and predicates have distinct uninterpreted types.\r
+ ** One pass is made through the input assertions, while a union-find data structure\r
+ ** maintains necessary information regarding constraints on these types.\r
+ **/\r
+\r
+#include <vector>\r
+\r
+#include "util/sort_inference.h"\r
+\r
+using namespace CVC4;\r
+using namespace std;\r
+\r
+namespace CVC4 {\r
+\r
+\r
+void SortInference::printSort( const char* c, int t ){\r
+ int rt = getRepresentative( t );\r
+ if( d_type_types.find( rt )!=d_type_types.end() ){\r
+ Trace(c) << d_type_types[rt];\r
+ }else{\r
+ Trace(c) << "s_" << rt;\r
+ }\r
+}\r
+\r
+void SortInference::simplify( std::vector< Node >& assertions, bool doRewrite ){\r
+ //process all assertions\r
+ for( unsigned i=0; i<assertions.size(); i++ ){\r
+ Trace("sort-inference-debug") << "Process " << assertions[i] << std::endl;\r
+ std::map< Node, Node > var_bound;\r
+ process( assertions[i], var_bound );\r
+ }\r
+ //print debug\r
+ if( Trace.isOn("sort-inference") ){\r
+ for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){\r
+ Trace("sort-inference") << it->first << " : ";\r
+ if( !d_op_arg_types[ it->first ].empty() ){\r
+ Trace("sort-inference") << "( ";\r
+ for( size_t i=0; i<d_op_arg_types[ it->first ].size(); i++ ){\r
+ printSort( "sort-inference", d_op_arg_types[ it->first ][i] );\r
+ Trace("sort-inference") << " ";\r
+ }\r
+ Trace("sort-inference") << ") -> ";\r
+ }\r
+ printSort( "sort-inference", it->second );\r
+ Trace("sort-inference") << std::endl;\r
+ }\r
+ }\r
+ if( doRewrite ){\r
+ //simplify all assertions by introducing new symbols wherever necessary (NOTE: this is unsound for quantifiers)\r
+ for( unsigned i=0; i<assertions.size(); i++ ){\r
+ std::map< Node, Node > var_bound;\r
+ assertions[i] = simplify( assertions[i], var_bound );\r
+ Trace("sort-inference-rewrite") << " --> " << assertions[i] << std::endl;\r
+ }\r
+ //now, ensure constants are distinct\r
+ for( std::map< TypeNode, std::map< Node, Node > >::iterator it = d_const_map.begin(); it != d_const_map.end(); ++it ){\r
+ std::vector< Node > consts;\r
+ for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){\r
+ consts.push_back( it2->second );\r
+ }\r
+ //add lemma enforcing introduced constants to be distinct?\r
+ }\r
+ }\r
+}\r
+\r
+int SortInference::getRepresentative( int t ){\r
+ std::map< int, int >::iterator it = d_type_union_find.find( t );\r
+ if( it!=d_type_union_find.end() ){\r
+ if( it->second==t ){\r
+ return t;\r
+ }else{\r
+ int rt = getRepresentative( it->second );\r
+ d_type_union_find[t] = rt;\r
+ return rt;\r
+ }\r
+ }else{\r
+ return t;\r
+ }\r
+}\r
+\r
+void SortInference::setEqual( int t1, int t2 ){\r
+ if( t1!=t2 ){\r
+ int rt1 = getRepresentative( t1 );\r
+ int rt2 = getRepresentative( t2 );\r
+ if( rt1!=rt2 ){\r
+ Trace("sort-inference-debug") << "Set equal : ";\r
+ printSort( "sort-inference-debug", rt1 );\r
+ Trace("sort-inference-debug") << " ";\r
+ printSort( "sort-inference-debug", rt2 );\r
+ Trace("sort-inference-debug") << std::endl;\r
+ //check if they must be a type\r
+ std::map< int, TypeNode >::iterator it1 = d_type_types.find( rt1 );\r
+ std::map< int, TypeNode >::iterator it2 = d_type_types.find( rt2 );\r
+ if( it2!=d_type_types.end() ){\r
+ if( it1==d_type_types.end() ){\r
+ //swap sides\r
+ int swap = rt1;\r
+ rt1 = rt2;\r
+ rt2 = swap;\r
+ }else{\r
+ Assert( rt1==rt2 );\r
+ }\r
+ }\r
+ /*\r
+ d_type_eq_class[rt1].insert( d_type_eq_class[rt1].end(), d_type_eq_class[rt2].begin(), d_type_eq_class[rt2].end() );\r
+ d_type_eq_class[rt2].clear();\r
+ Trace("sort-inference-debug") << "EqClass : { ";\r
+ for( int i=0; i<(int)d_type_eq_class[rt1].size(); i++ ){\r
+ Trace("sort-inference-debug") << d_type_eq_class[rt1][i] << ", ";\r
+ }\r
+ Trace("sort-inference-debug") << "}" << std::endl;\r
+ */\r
+ d_type_union_find[rt2] = rt1;\r
+ }\r
+ }\r
+}\r
+\r
+int SortInference::getIdForType( TypeNode tn ){\r
+ //register the return type\r
+ std::map< TypeNode, int >::iterator it = d_id_for_types.find( tn );\r
+ if( it==d_id_for_types.end() ){\r
+ int sc = sortCount;\r
+ d_type_types[ sortCount ] = tn;\r
+ d_id_for_types[ tn ] = sortCount;\r
+ sortCount++;\r
+ return sc;\r
+ }else{\r
+ return it->second;\r
+ }\r
+}\r
+\r
+int SortInference::process( Node n, std::map< Node, Node >& var_bound ){\r
+ Trace("sort-inference-debug") << "Process " << n << std::endl;\r
+ //add to variable bindings\r
+ if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){\r
+ for( size_t i=0; i<n[0].getNumChildren(); i++ ){\r
+ //TODO: try applying sort inference to quantified variables\r
+ //d_var_types[n][ n[0][i] ] = sortCount;\r
+ //sortCount++;\r
+\r
+ //type of the quantified variable must be the same\r
+ d_var_types[n][ n[0][i] ] = getIdForType( n[0][i].getType() );\r
+ var_bound[ n[0][i] ] = n;\r
+ }\r
+ }\r
+\r
+ //process children\r
+ std::vector< Node > children;\r
+ std::vector< int > child_types;\r
+ for( size_t i=0; i<n.getNumChildren(); i++ ){\r
+ bool processChild = true;\r
+ if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){\r
+ processChild = i==1;\r
+ }\r
+ if( processChild ){\r
+ children.push_back( n[i] );\r
+ child_types.push_back( process( n[i], var_bound ) );\r
+ }\r
+ }\r
+\r
+ //remove from variable bindings\r
+ if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){\r
+ //erase from variable bound\r
+ for( size_t i=0; i<n[0].getNumChildren(); i++ ){\r
+ var_bound.erase( n[0][i] );\r
+ }\r
+ }\r
+\r
+ int retType;\r
+ if( n.getKind()==kind::EQUAL ){\r
+ //we only require that the left and right hand side must be equal\r
+ setEqual( child_types[0], child_types[1] );\r
+ retType = getIdForType( n.getType() );\r
+ }else if( n.getKind()==kind::APPLY_UF ){\r
+ Node op = n.getOperator();\r
+ if( d_op_return_types.find( op )==d_op_return_types.end() ){\r
+ //assign arbitrary sort for return type\r
+ d_op_return_types[op] = sortCount;\r
+ sortCount++;\r
+ //d_type_eq_class[sortCount].push_back( op );\r
+ //assign arbitrary sort for argument types\r
+ for( size_t i=0; i<n.getNumChildren(); i++ ){\r
+ d_op_arg_types[op].push_back( sortCount );\r
+ sortCount++;\r
+ }\r
+ }\r
+ for( size_t i=0; i<n.getNumChildren(); i++ ){\r
+ //the argument of the operator must match the return type of the subterm\r
+ setEqual( child_types[i], d_op_arg_types[op][i] );\r
+ }\r
+ //return type is the return type\r
+ retType = d_op_return_types[op];\r
+ }else{\r
+ std::map< Node, Node >::iterator it = var_bound.find( n );\r
+ if( it!=var_bound.end() ){\r
+ Trace("sort-inference-debug") << n << " is a bound variable." << std::endl;\r
+ //the return type was specified while binding\r
+ retType = d_var_types[it->second][n];\r
+ }else if( n.getKind() == kind::VARIABLE ){\r
+ Trace("sort-inference-debug") << n << " is a variable." << std::endl;\r
+ if( d_op_return_types.find( n )==d_op_return_types.end() ){\r
+ //assign arbitrary sort\r
+ d_op_return_types[n] = sortCount;\r
+ sortCount++;\r
+ //d_type_eq_class[sortCount].push_back( n );\r
+ }\r
+ retType = d_op_return_types[n];\r
+ }else if( n.isConst() ){\r
+ Trace("sort-inference-debug") << n << " is a constant." << std::endl;\r
+ //can be any type we want\r
+ retType = sortCount;\r
+ sortCount++;\r
+ }else{\r
+ Trace("sort-inference-debug") << n << " is a interpreted symbol." << std::endl;\r
+ //it is an interpretted term\r
+ for( size_t i=0; i<children.size(); i++ ){\r
+ Trace("sort-inference-debug") << children[i] << " forced to have " << children[i].getType() << std::endl;\r
+ //must enforce the actual type of the operator on the children\r
+ int ct = getIdForType( children[i].getType() );\r
+ setEqual( child_types[i], ct );\r
+ }\r
+ //return type must be the actual return type\r
+ retType = getIdForType( n.getType() );\r
+ }\r
+ }\r
+ Trace("sort-inference-debug") << "Type( " << n << " ) = ";\r
+ printSort("sort-inference-debug", retType );\r
+ Trace("sort-inference-debug") << std::endl;\r
+ return retType;\r
+}\r
+\r
+\r
+TypeNode SortInference::getOrCreateTypeForId( int t, TypeNode pref ){\r
+ int rt = getRepresentative( t );\r
+ if( d_type_types.find( rt )!=d_type_types.end() ){\r
+ return d_type_types[rt];\r
+ }else{\r
+ TypeNode retType;\r
+ //see if we can assign pref\r
+ if( !pref.isNull() && d_id_for_types.find( pref )==d_id_for_types.end() ){\r
+ retType = pref;\r
+ }else{\r
+ if( d_subtype_count.find( pref )==d_subtype_count.end() ){\r
+ d_subtype_count[pref] = 0;\r
+ }\r
+ //must create new type\r
+ std::stringstream ss;\r
+ ss << "it_" << d_subtype_count[pref] << "_" << pref;\r
+ d_subtype_count[pref]++;\r
+ retType = NodeManager::currentNM()->mkSort( ss.str() );\r
+ }\r
+ d_id_for_types[ retType ] = rt;\r
+ d_type_types[ rt ] = retType;\r
+ return retType;\r
+ }\r
+}\r
+\r
+TypeNode SortInference::getTypeForId( int t ){\r
+ int rt = getRepresentative( t );\r
+ if( d_type_types.find( rt )!=d_type_types.end() ){\r
+ return d_type_types[rt];\r
+ }else{\r
+ return TypeNode::null();\r
+ }\r
+}\r
+\r
+Node SortInference::getNewSymbol( Node old, TypeNode tn ){\r
+ if( tn==old.getType() ){\r
+ return old;\r
+ }else{\r
+ std::stringstream ss;\r
+ ss << "i_$$_" << old;\r
+ return NodeManager::currentNM()->mkSkolem( ss.str(), tn, "created during sort inference" );\r
+ }\r
+}\r
+\r
+Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){\r
+ std::vector< Node > children;\r
+ if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){\r
+ //recreate based on types of variables\r
+ std::vector< Node > new_children;\r
+ for( size_t i=0; i<n[0].getNumChildren(); i++ ){\r
+ TypeNode tn = getOrCreateTypeForId( d_var_types[n][ n[0][i] ], n[0][i].getType() );\r
+ Node v = getNewSymbol( n[0][i], tn );\r
+ new_children.push_back( v );\r
+ var_bound[ n[0][i] ] = v;\r
+ }\r
+ children.push_back( NodeManager::currentNM()->mkNode( n[0].getKind(), new_children ) );\r
+ }\r
+\r
+ //process children\r
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){\r
+ children.push_back( n.getOperator() );\r
+ }\r
+ for( size_t i=0; i<n.getNumChildren(); i++ ){\r
+ bool processChild = true;\r
+ if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){\r
+ processChild = i>=1;\r
+ }\r
+ if( processChild ){\r
+ children.push_back( simplify( n[i], var_bound ) );\r
+ }\r
+ }\r
+\r
+ //remove from variable bindings\r
+ if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){\r
+ //erase from variable bound\r
+ for( size_t i=0; i<n[0].getNumChildren(); i++ ){\r
+ var_bound.erase( n[0][i] );\r
+ }\r
+ return NodeManager::currentNM()->mkNode( n.getKind(), children );\r
+ }else if( n.getKind()==kind::APPLY_UF ){\r
+ Node op = n.getOperator();\r
+ if( d_symbol_map.find( op )==d_symbol_map.end() ){\r
+ //make the new operator if necessary\r
+ bool opChanged = false;\r
+ std::vector< TypeNode > argTypes;\r
+ for( size_t i=0; i<n.getNumChildren(); i++ ){\r
+ TypeNode tn = getOrCreateTypeForId( d_op_arg_types[op][i], n[i].getType() );\r
+ argTypes.push_back( tn );\r
+ if( tn!=n[i].getType() ){\r
+ opChanged = true;\r
+ }\r
+ }\r
+ TypeNode retType = getOrCreateTypeForId( d_op_return_types[op], n.getType() );\r
+ if( retType!=n.getType() ){\r
+ opChanged = true;\r
+ }\r
+ if( opChanged ){\r
+ std::stringstream ss;\r
+ ss << "io_$$_" << op;\r
+ TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, retType );\r
+ d_symbol_map[op] = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during sort inference" );\r
+ }else{\r
+ d_symbol_map[op] = op;\r
+ }\r
+ }\r
+ children[0] = d_symbol_map[op];\r
+ //make sure all children have been taken care of\r
+ for( size_t i=0; i<n.getNumChildren(); i++ ){\r
+ TypeNode tn = children[i+1].getType();\r
+ TypeNode tna = getTypeForId( d_op_arg_types[op][i] );\r
+ if( tn!=tna ){\r
+ if( n[i].isConst() ){\r
+ //must make constant of type tna\r
+ if( d_const_map[tna].find( n[i] )==d_const_map[tna].end() ){\r
+ std::stringstream ss;\r
+ ss << "ic_" << tna << "_" << n[i];\r
+ d_const_map[tna][ n[i] ] = NodeManager::currentNM()->mkSkolem( ss.str(), tna, "constant created during sort inference" ); //use mkConst???\r
+ }\r
+ children[i+1] = d_const_map[tna][ n[i] ];\r
+ }else{\r
+ Trace("sort-inference-warn") << "Sort inference created bad child: " << n[i] << " " << tn << " " << tna << std::endl;\r
+ Assert( false );\r
+ }\r
+ }\r
+ }\r
+ return NodeManager::currentNM()->mkNode( kind::APPLY_UF, children );\r
+ }else{\r
+ std::map< Node, Node >::iterator it = var_bound.find( n );\r
+ if( it!=var_bound.end() ){\r
+ return it->second;\r
+ }else if( n.getKind() == kind::VARIABLE ){\r
+ if( d_symbol_map.find( n )==d_symbol_map.end() ){\r
+ TypeNode tn = getOrCreateTypeForId( d_op_return_types[n], n.getType() );\r
+ d_symbol_map[n] = getNewSymbol( n, tn );\r
+ }\r
+ return d_symbol_map[n];\r
+ }else if( n.isConst() ){\r
+ //just return n, we will fix at higher scope\r
+ return n;\r
+ }else{\r
+ return NodeManager::currentNM()->mkNode( n.getKind(), children );\r
+ }\r
+ }\r
+\r
+}\r
+\r
+}\r
--- /dev/null
+/********************* */\r
+/*! \file sort_inference.h\r
+ ** \verbatim\r
+ ** Original author: ajreynol\r
+ ** Major contributors: none\r
+ ** Minor contributors (to current version): none\r
+ ** This file is part of the CVC4 prototype.\r
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief Pre-process step for performing sort inference\r
+ **/\r
+\r
+#include "cvc4_private.h"\r
+\r
+#ifndef __CVC4__SORT_INFERENCE_H\r
+#define __CVC4__SORT_INFERENCE_H\r
+\r
+#include <iostream>\r
+#include <string>\r
+#include <vector>\r
+#include <map>\r
+#include "expr/node.h"\r
+#include "expr/type_node.h"\r
+\r
+namespace CVC4 {\r
+\r
+class SortInference{\r
+private:\r
+ //for debugging\r
+ //std::map< int, std::vector< Node > > d_type_eq_class;\r
+private:\r
+ int sortCount;\r
+ std::map< int, int > d_type_union_find;\r
+ std::map< int, TypeNode > d_type_types;\r
+ std::map< TypeNode, int > d_id_for_types;\r
+ //for apply uf operators\r
+ std::map< Node, int > d_op_return_types;\r
+ std::map< Node, std::vector< int > > d_op_arg_types;\r
+ //for bound variables\r
+ std::map< Node, std::map< Node, int > > d_var_types;\r
+ //get representative\r
+ int getRepresentative( int t );\r
+ void setEqual( int t1, int t2 );\r
+ int getIdForType( TypeNode tn );\r
+ void printSort( const char* c, int t );\r
+ //process\r
+ int process( Node n, std::map< Node, Node >& var_bound );\r
+private:\r
+ //mapping from old symbols to new symbols\r
+ std::map< Node, Node > d_symbol_map;\r
+ //mapping from constants to new symbols\r
+ std::map< TypeNode, std::map< Node, Node > > d_const_map;\r
+ //number of subtypes generated\r
+ std::map< TypeNode, int > d_subtype_count;\r
+ //helper functions for simplify\r
+ TypeNode getOrCreateTypeForId( int t, TypeNode pref );\r
+ TypeNode getTypeForId( int t );\r
+ Node getNewSymbol( Node old, TypeNode tn );\r
+ //simplify\r
+ Node simplify( Node n, std::map< Node, Node >& var_bound );\r
+public:\r
+ SortInference() : sortCount( 0 ){}\r
+ ~SortInference(){}\r
+\r
+ void simplify( std::vector< Node >& assertions, bool doRewrite = false );\r
+};\r
+\r
+}\r
+\r
+#endif\r
projects / cvc5.git / commitdiff