summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rwxr-xr-xsrc/theory/quantifiers/inst_match_generator.cpp2
-rw-r--r--src/theory/quantifiers/model_engine.cpp153
-rw-r--r--src/theory/quantifiers/options1
-rw-r--r--src/theory/quantifiers/trigger.cpp14
-rw-r--r--src/theory/rep_set.cpp17
-rw-r--r--src/theory/rep_set.h6
-rw-r--r--src/theory/uf/options6
-rw-r--r--src/theory/uf/theory_uf_strong_solver.cpp60
8 files changed, 135 insertions, 124 deletions
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; i<fm->getNumAssertedQuantifiers(); 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; 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;
}
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; i<f[0].getNumChildren(); i++ ){
d_types.push_back( f[0][i].getType() );
}
- initialize();
+ return initialize();
}
-void RepSetIterator::setFunctionDomain( Node op ){
+bool RepSetIterator::setFunctionDomain( Node op ){
Assert( d_types.empty() );
TypeNode tn = op.getType();
for( size_t i=0; i<tn.getNumChildren()-1; i++ ){
d_types.push_back( tn[i] );
}
- initialize();
+ return initialize();
}
-void RepSetIterator::initialize(){
+bool RepSetIterator::initialize(){
for( size_t i=0; i<d_types.size(); i++ ){
d_index.push_back( 0 );
//store default index order
@@ -146,7 +146,7 @@ void RepSetIterator::initialize(){
d_incomplete = true;
}
}else{
- Trace("fmf-incomplete") << "Incomplete because of type " << tn << std::endl;
+ Trace("fmf-incomplete") << "Incomplete because of unknown type " << tn << std::endl;
d_incomplete = true;
}
if( d_rep_set->hasType( 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;
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback