From 0ba075e240b2083163ab35a3580547cae6927b6c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 12 Nov 2012 16:46:51 +0000 Subject: minor bug fixes for quantifiers, added sort inference module (not ready to be used yet), added new totality lemma option for uf strong solver --- src/printer/smt2/smt2_printer.cpp | 3 +- src/smt/options | 3 + src/smt/smt_engine.cpp | 11 +- src/theory/quantifiers/inst_match_generator.cpp | 2 +- src/theory/quantifiers/model_engine.cpp | 153 ++++----- src/theory/quantifiers/options | 1 + src/theory/quantifiers/trigger.cpp | 14 +- src/theory/rep_set.cpp | 17 +- src/theory/rep_set.h | 6 +- src/theory/uf/options | 6 +- src/theory/uf/theory_uf_strong_solver.cpp | 60 ++-- src/util/Makefile.am | 4 +- src/util/sort_inference.cpp | 393 ++++++++++++++++++++++++ src/util/sort_inference.h | 72 +++++ 14 files changed, 617 insertions(+), 128 deletions(-) create mode 100755 src/util/sort_inference.cpp create mode 100755 src/util/sort_inference.h (limited to 'src') diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index a66134e0d..bf222d189 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -295,8 +295,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, 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 diff --git a/src/smt/options b/src/smt/options index ab903c951..a3038cd4e 100644 --- a/src/smt/options +++ b/src/smt/options @@ -46,6 +46,9 @@ option unconstrainedSimp --unconstrained-simp bool :default false :read-write 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 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ee0d9debc..e0d7c8e98 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -63,6 +63,7 @@ #include "printer/printer.h" #include "prop/options.h" #include "theory/arrays/options.h" +#include "util/sort_inference.h" using namespace std; using namespace CVC4; @@ -898,7 +899,7 @@ void SmtEngine::setLogicInternal() throw() { if (options::checkModels()) { Warning() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << std::endl; setOption("check-models", SExpr("false")); - } + } } } @@ -1298,6 +1299,7 @@ Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vect }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() ); @@ -1965,6 +1967,13 @@ void SmtEnginePrivate::processAssertions() { } 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(); diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index acd733e22..a70fd9d7e 100755 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -122,7 +122,7 @@ void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){ d_cg = new CandidateGeneratorQueue; if( !Trigger::getPatternArithmetic( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){ Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; - Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; + //Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; d_matchPolicy = MATCH_GEN_INTERNAL_ERROR; }else{ Debug("matching-arith") << "Generated arithmetic pattern for " << d_match_pattern << ": " << std::endl; diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index defb58bf2..456914818 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -157,7 +157,7 @@ int ModelEngine::checkModel( int checkOption ){ 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() ){ @@ -180,7 +180,7 @@ int ModelEngine::checkModel( int checkOption ){ 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; igetNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); //keep track of total instantiations for statistics @@ -235,88 +235,89 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ //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; igetTermDatabase()->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; igetTermDatabase()->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; i1000 ){ + 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; i1000 ){ - 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; } diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 5802a05cd..2c36520e4 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -91,4 +91,5 @@ option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :defau 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 diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 553189d13..ae08fe863 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -459,13 +459,15 @@ bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coef 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; diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 2770a4e77..b50878e70 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -99,25 +99,25 @@ RepSetIterator::RepSetIterator( RepSet* rs ) : d_rep_set( rs ){ } -void RepSetIterator::setQuantifier( Node f ){ +bool RepSetIterator::setQuantifier( Node f ){ Assert( d_types.empty() ); //store indicies for( size_t i=0; ihasType( tn ) ){ @@ -154,11 +154,10 @@ void RepSetIterator::initialize(){ d_domain[i].push_back( j ); } }else{ - Trace("fmf-incomplete") << "Incomplete, unknown type " << tn << std::endl; - d_incomplete = true; - Unimplemented("Cannot create representative set iterator for unknown type quantifier"); + return false; } } + return true; } void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){ diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index 8e7da4ce5..61b2ebf9f 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -54,14 +54,14 @@ typedef std::vector< int > RepDomain; class RepSetIterator { private: //initialize function - void initialize(); + bool initialize(); public: RepSetIterator( RepSet* rs ); ~RepSetIterator(){} //set that this iterator will be iterating over instantiations for a quantifier - void setQuantifier( Node f ); + bool setQuantifier( Node f ); //set that this iterator will be iterating over the domain of a function - void setFunctionDomain( Node op ); + bool setFunctionDomain( Node op ); public: //pointer to model RepSet* d_rep_set; diff --git a/src/theory/uf/options b/src/theory/uf/options index 0799ba4d5..2569ccbff 100644 --- a/src/theory/uf/options +++ b/src/theory/uf/options @@ -15,15 +15,15 @@ option ufssEagerSplits --uf-ss-eager-split bool :default false 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 diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 548d6f2f0..edeb6b6ec 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -561,19 +561,8 @@ void StrongSolverTheoryUf::SortRepModel::check( Theory::Effort level, OutputChan } 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 ){ @@ -587,8 +576,21 @@ void StrongSolverTheoryUf::SortRepModel::check( Theory::Effort level, OutputChan } } } - 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 @@ -768,6 +770,7 @@ void StrongSolverTheoryUf::SortRepModel::assertCardinality( OutputChannel* out, } } }else{ + /* if( options::ufssModelInference() ){ //check if we are at decision level 0 if( d_th->d_valuation.getAssertionLevel()==0 ){ @@ -781,6 +784,7 @@ void StrongSolverTheoryUf::SortRepModel::assertCardinality( OutputChannel* out, } } } + */ //see if we need to request a new cardinality if( !d_hasCard ){ bool needsCard = true; @@ -915,15 +919,15 @@ void StrongSolverTheoryUf::SortRepModel::allocateCardinality( OutputChannel* out 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 ); @@ -1026,7 +1030,8 @@ void StrongSolverTheoryUf::SortRepModel::addCliqueLemma( std::vector< Node >& cl 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 ); @@ -1141,16 +1146,16 @@ void StrongSolverTheoryUf::SortRepModel::addTotalityAxiom( Node n, int cardinali /** 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 ){ @@ -1467,12 +1472,13 @@ Node StrongSolverTheoryUf::getNextDecisionRequest(){ } 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 ); @@ -1497,6 +1503,8 @@ void StrongSolverTheoryUf::preRegisterTerm( TNode n ){ d_rep_model[tn] = rm; d_rep_model_init[tn] = true; } + }else{ + Trace("uf-ss-register") << "Already preregistered sort " << tn << "." << std::endl; } } diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 098024912..aa122905b 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -84,7 +84,9 @@ libutil_la_SOURCES = \ 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 diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp new file mode 100755 index 000000000..5dc60dbb0 --- /dev/null +++ b/src/util/sort_inference.cpp @@ -0,0 +1,393 @@ +/********************* */ +/*! \file sort_inference.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Sort inference module + ** + ** This class implements sort inference, based on a simple algorithm: + ** First, we assume all functions and predicates have distinct uninterpreted types. + ** One pass is made through the input assertions, while a union-find data structure + ** maintains necessary information regarding constraints on these types. + **/ + +#include + +#include "util/sort_inference.h" + +using namespace CVC4; +using namespace std; + +namespace CVC4 { + + +void SortInference::printSort( const char* c, int t ){ + int rt = getRepresentative( t ); + if( d_type_types.find( rt )!=d_type_types.end() ){ + Trace(c) << d_type_types[rt]; + }else{ + Trace(c) << "s_" << rt; + } +} + +void SortInference::simplify( std::vector< Node >& assertions, bool doRewrite ){ + //process all assertions + for( unsigned i=0; i var_bound; + process( assertions[i], var_bound ); + } + //print debug + if( Trace.isOn("sort-inference") ){ + for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){ + Trace("sort-inference") << it->first << " : "; + if( !d_op_arg_types[ it->first ].empty() ){ + Trace("sort-inference") << "( "; + for( size_t i=0; ifirst ].size(); i++ ){ + printSort( "sort-inference", d_op_arg_types[ it->first ][i] ); + Trace("sort-inference") << " "; + } + Trace("sort-inference") << ") -> "; + } + printSort( "sort-inference", it->second ); + Trace("sort-inference") << std::endl; + } + } + if( doRewrite ){ + //simplify all assertions by introducing new symbols wherever necessary (NOTE: this is unsound for quantifiers) + for( unsigned i=0; i var_bound; + assertions[i] = simplify( assertions[i], var_bound ); + Trace("sort-inference-rewrite") << " --> " << assertions[i] << std::endl; + } + //now, ensure constants are distinct + for( std::map< TypeNode, std::map< Node, Node > >::iterator it = d_const_map.begin(); it != d_const_map.end(); ++it ){ + std::vector< Node > consts; + for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + consts.push_back( it2->second ); + } + //add lemma enforcing introduced constants to be distinct? + } + } +} + +int SortInference::getRepresentative( int t ){ + std::map< int, int >::iterator it = d_type_union_find.find( t ); + if( it!=d_type_union_find.end() ){ + if( it->second==t ){ + return t; + }else{ + int rt = getRepresentative( it->second ); + d_type_union_find[t] = rt; + return rt; + } + }else{ + return t; + } +} + +void SortInference::setEqual( int t1, int t2 ){ + if( t1!=t2 ){ + int rt1 = getRepresentative( t1 ); + int rt2 = getRepresentative( t2 ); + if( rt1!=rt2 ){ + Trace("sort-inference-debug") << "Set equal : "; + printSort( "sort-inference-debug", rt1 ); + Trace("sort-inference-debug") << " "; + printSort( "sort-inference-debug", rt2 ); + Trace("sort-inference-debug") << std::endl; + //check if they must be a type + std::map< int, TypeNode >::iterator it1 = d_type_types.find( rt1 ); + std::map< int, TypeNode >::iterator it2 = d_type_types.find( rt2 ); + if( it2!=d_type_types.end() ){ + if( it1==d_type_types.end() ){ + //swap sides + int swap = rt1; + rt1 = rt2; + rt2 = swap; + }else{ + Assert( rt1==rt2 ); + } + } + /* + d_type_eq_class[rt1].insert( d_type_eq_class[rt1].end(), d_type_eq_class[rt2].begin(), d_type_eq_class[rt2].end() ); + d_type_eq_class[rt2].clear(); + Trace("sort-inference-debug") << "EqClass : { "; + for( int i=0; i<(int)d_type_eq_class[rt1].size(); i++ ){ + Trace("sort-inference-debug") << d_type_eq_class[rt1][i] << ", "; + } + Trace("sort-inference-debug") << "}" << std::endl; + */ + d_type_union_find[rt2] = rt1; + } + } +} + +int SortInference::getIdForType( TypeNode tn ){ + //register the return type + std::map< TypeNode, int >::iterator it = d_id_for_types.find( tn ); + if( it==d_id_for_types.end() ){ + int sc = sortCount; + d_type_types[ sortCount ] = tn; + d_id_for_types[ tn ] = sortCount; + sortCount++; + return sc; + }else{ + return it->second; + } +} + +int SortInference::process( Node n, std::map< Node, Node >& var_bound ){ + Trace("sort-inference-debug") << "Process " << n << std::endl; + //add to variable bindings + if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ + for( size_t i=0; i children; + std::vector< int > child_types; + for( size_t i=0; i::iterator it = var_bound.find( n ); + if( it!=var_bound.end() ){ + Trace("sort-inference-debug") << n << " is a bound variable." << std::endl; + //the return type was specified while binding + retType = d_var_types[it->second][n]; + }else if( n.getKind() == kind::VARIABLE ){ + Trace("sort-inference-debug") << n << " is a variable." << std::endl; + if( d_op_return_types.find( n )==d_op_return_types.end() ){ + //assign arbitrary sort + d_op_return_types[n] = sortCount; + sortCount++; + //d_type_eq_class[sortCount].push_back( n ); + } + retType = d_op_return_types[n]; + }else if( n.isConst() ){ + Trace("sort-inference-debug") << n << " is a constant." << std::endl; + //can be any type we want + retType = sortCount; + sortCount++; + }else{ + Trace("sort-inference-debug") << n << " is a interpreted symbol." << std::endl; + //it is an interpretted term + for( size_t i=0; imkSort( ss.str() ); + } + d_id_for_types[ retType ] = rt; + d_type_types[ rt ] = retType; + return retType; + } +} + +TypeNode SortInference::getTypeForId( int t ){ + int rt = getRepresentative( t ); + if( d_type_types.find( rt )!=d_type_types.end() ){ + return d_type_types[rt]; + }else{ + return TypeNode::null(); + } +} + +Node SortInference::getNewSymbol( Node old, TypeNode tn ){ + if( tn==old.getType() ){ + return old; + }else{ + std::stringstream ss; + ss << "i_$$_" << old; + return NodeManager::currentNM()->mkSkolem( ss.str(), tn, "created during sort inference" ); + } +} + +Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ + std::vector< Node > children; + if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ + //recreate based on types of variables + std::vector< Node > new_children; + for( size_t i=0; imkNode( n[0].getKind(), new_children ) ); + } + + //process children + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + for( size_t i=0; i=1; + } + if( processChild ){ + children.push_back( simplify( n[i], var_bound ) ); + } + } + + //remove from variable bindings + if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ + //erase from variable bound + for( size_t i=0; imkNode( n.getKind(), children ); + }else if( n.getKind()==kind::APPLY_UF ){ + Node op = n.getOperator(); + if( d_symbol_map.find( op )==d_symbol_map.end() ){ + //make the new operator if necessary + bool opChanged = false; + std::vector< TypeNode > argTypes; + for( size_t i=0; imkFunctionType( argTypes, retType ); + d_symbol_map[op] = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during sort inference" ); + }else{ + d_symbol_map[op] = op; + } + } + children[0] = d_symbol_map[op]; + //make sure all children have been taken care of + for( size_t i=0; imkSkolem( ss.str(), tna, "constant created during sort inference" ); //use mkConst??? + } + children[i+1] = d_const_map[tna][ n[i] ]; + }else{ + Trace("sort-inference-warn") << "Sort inference created bad child: " << n[i] << " " << tn << " " << tna << std::endl; + Assert( false ); + } + } + } + return NodeManager::currentNM()->mkNode( kind::APPLY_UF, children ); + }else{ + std::map< Node, Node >::iterator it = var_bound.find( n ); + if( it!=var_bound.end() ){ + return it->second; + }else if( n.getKind() == kind::VARIABLE ){ + if( d_symbol_map.find( n )==d_symbol_map.end() ){ + TypeNode tn = getOrCreateTypeForId( d_op_return_types[n], n.getType() ); + d_symbol_map[n] = getNewSymbol( n, tn ); + } + return d_symbol_map[n]; + }else if( n.isConst() ){ + //just return n, we will fix at higher scope + return n; + }else{ + return NodeManager::currentNM()->mkNode( n.getKind(), children ); + } + } + +} + +} diff --git a/src/util/sort_inference.h b/src/util/sort_inference.h new file mode 100755 index 000000000..363dbd84d --- /dev/null +++ b/src/util/sort_inference.h @@ -0,0 +1,72 @@ +/********************* */ +/*! \file sort_inference.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Pre-process step for performing sort inference + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__SORT_INFERENCE_H +#define __CVC4__SORT_INFERENCE_H + +#include +#include +#include +#include +#include "expr/node.h" +#include "expr/type_node.h" + +namespace CVC4 { + +class SortInference{ +private: + //for debugging + //std::map< int, std::vector< Node > > d_type_eq_class; +private: + int sortCount; + std::map< int, int > d_type_union_find; + std::map< int, TypeNode > d_type_types; + std::map< TypeNode, int > d_id_for_types; + //for apply uf operators + std::map< Node, int > d_op_return_types; + std::map< Node, std::vector< int > > d_op_arg_types; + //for bound variables + std::map< Node, std::map< Node, int > > d_var_types; + //get representative + int getRepresentative( int t ); + void setEqual( int t1, int t2 ); + int getIdForType( TypeNode tn ); + void printSort( const char* c, int t ); + //process + int process( Node n, std::map< Node, Node >& var_bound ); +private: + //mapping from old symbols to new symbols + std::map< Node, Node > d_symbol_map; + //mapping from constants to new symbols + std::map< TypeNode, std::map< Node, Node > > d_const_map; + //number of subtypes generated + std::map< TypeNode, int > d_subtype_count; + //helper functions for simplify + TypeNode getOrCreateTypeForId( int t, TypeNode pref ); + TypeNode getTypeForId( int t ); + Node getNewSymbol( Node old, TypeNode tn ); + //simplify + Node simplify( Node n, std::map< Node, Node >& var_bound ); +public: + SortInference() : sortCount( 0 ){} + ~SortInference(){} + + void simplify( std::vector< Node >& assertions, bool doRewrite = false ); +}; + +} + +#endif -- cgit v1.2.3