read_only = true
help = "mode of operation for uf strong solver."
-[[option]]
- name = "ufssCliqueSplits"
- category = "regular"
- long = "uf-ss-clique-splits"
- type = "bool"
- default = "false"
- read_only = true
- help = "use cliques instead of splitting on demand to shrink model"
-
[[option]]
name = "ufssFairness"
category = "regular"
}
Node InstMatch::get(int i) const { return d_vals[i]; }
-void InstMatch::getInst(std::vector<Node>& inst) const
-{
- inst.insert(inst.end(), d_vals.begin(), d_vals.end());
-}
void InstMatch::setValue( int i, TNode n ) {
d_vals[i] = n;
}
/** get the i^th term in the instantiation */
Node get(int i) const;
- /** append the terms of this instantiation to inst */
- void getInst(std::vector<Node>& inst) const;
/** set/overwrites the i^th field in the instantiation with n */
void setValue( int i, TNode n );
/** set the i^th term in the instantiation to n
std::vector<Node> syms;
computeSymbols(f[1], syms);
d_syms[f].insert(d_syms[f].begin(), syms.begin(), syms.end());
- // set initial relevance
- int minRelevance = -1;
- for (int i = 0; i < (int)syms.size(); i++)
- {
- d_syms_quants[syms[i]].push_back(f);
- int r = getRelevance(syms[i]);
- if (r != -1 && (minRelevance == -1 || r < minRelevance))
- {
- minRelevance = r;
- }
- }
- if (minRelevance != -1)
- {
- setRelevance(f, minRelevance + 1);
- }
}
/** compute symbols */
}
}
-/** set relevance */
-void QuantRelevance::setRelevance(Node s, int r)
-{
- if (d_computeRel)
- {
- int rOld = getRelevance(s);
- if (rOld == -1 || r < rOld)
- {
- d_relevance[s] = r;
- if (s.getKind() == FORALL)
- {
- for (int i = 0; i < (int)d_syms[s].size(); i++)
- {
- setRelevance(d_syms[s][i], r);
- }
- }
- else
- {
- for (int i = 0; i < (int)d_syms_quants[s].size(); i++)
- {
- setRelevance(d_syms_quants[s][i], r + 1);
- }
- }
- }
- }
-}
-
} /* CVC4::theory::quantifiers namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
* if this is false, then all calls to getRelevance
* return -1.
*/
- QuantRelevance(bool cr) : d_computeRel(cr) {}
+ QuantRelevance() {}
~QuantRelevance() {}
/** reset */
bool reset(Theory::Effort e) override { return true; }
void registerQuantifier(Node q) override;
/** identify */
std::string identify() const override { return "QuantRelevance"; }
- /** set relevance of symbol s to r */
- void setRelevance(Node s, int r);
- /** get relevance of symbol s */
- int getRelevance(Node s)
- {
- return d_relevance.find(s) == d_relevance.end() ? -1 : d_relevance[s];
- }
/** get number of quantifiers for symbol s */
unsigned getNumQuantifiersForSymbol(Node s)
{
}
private:
- /** for computing relevance */
- bool d_computeRel;
/** map from quantifiers to symbols they contain */
std::map<Node, std::vector<Node> > d_syms;
/** map from symbols to quantifiers */
d_strategy[f].initialize(qe, f, enums);
}
-bool SygusUnif::constructSolution(std::vector<Node>& sols,
- std::vector<Node>& lemmas)
-{
- // initialize a call to construct solution
- initializeConstructSol();
- for (const Node& f : d_candidates)
- {
- // initialize a call to construct solution for function f
- initializeConstructSolFor(f);
- // call the virtual construct solution method
- Node e = d_strategy[f].getRootEnumerator();
- Node sol = constructSol(f, e, role_equal, 1, lemmas);
- if (sol.isNull())
- {
- return false;
- }
- sols.push_back(sol);
- }
- return true;
-}
-
Node SygusUnif::constructBestSolvedTerm(const std::vector<Node>& solved)
{
Assert(!solved.empty());
* channel by the caller.
*/
virtual bool constructSolution(std::vector<Node>& sols,
- std::vector<Node>& lemmas);
+ std::vector<Node>& lemmas) = 0;
protected:
/** reference to quantifier engine */
Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
if( options::relevantTriggers() ){
- d_quant_rel = new quantifiers::QuantRelevance(false);
+ d_quant_rel = new quantifiers::QuantRelevance;
d_util.push_back(d_quant_rel);
}else{
d_quant_rel = NULL;
}
if( e==Theory::EFFORT_LAST_CALL ){
- //if effort is last call, try to minimize model first
- //uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver();
- //if( ufss && !ufss->minimize() ){ return; }
++(d_statistics.d_instantiation_rounds_lc);
}else if( e==Theory::EFFORT_FULL ){
++(d_statistics.d_instantiation_rounds);
{
d_sygus_tdb->getEvalUnfold()->registerEvalTerm(n);
}
-
- // added contains also the Node that just have been asserted in this
- // branch
- if (d_quant_rel)
- {
- for (std::set<Node>::iterator i = added.begin(), end = added.end();
- i != end;
- i++)
- {
- d_quant_rel->setRelevance( i->getOperator(), 0 );
- }
- }
}
}
}
#include "theory/theory_model.h"
//#define ONE_SPLIT_REGION
-//#define DISABLE_QUICK_CLIQUE_CHECKS
//#define COMBINE_REGIONS_SMALL_INTO_LARGE
//#define LAZY_REL_EQC
return false;
}
-bool Region::getCandidateClique( int cardinality, std::vector< Node >& clique )
-{
- if( d_testCliqueSize>=unsigned(cardinality+1) ){
- //test clique is a clique
- for( NodeBoolMap::iterator it = d_testClique.begin();
- it != d_testClique.end(); ++it ){
- if( (*it).second ){
- clique.push_back( (*it).first );
- }
- }
- return true;
- }
- return false;
-}
-
void Region::getNumExternalDisequalities(
std::map< Node, int >& num_ext_disequalities ){
for( Region::iterator it = begin(); it != end(); ++it ){
//see if we have any recommended splits from large regions
for( int i=0; i<(int)d_regions_index; i++ ){
if( d_regions[i]->valid() && d_regions[i]->getNumReps()>d_cardinality ){
- //just add the clique lemma
- if( level==Theory::EFFORT_FULL && options::ufssCliqueSplits() ){
- std::vector< Node > clique;
- if( d_regions[i]->getCandidateClique( d_cardinality, clique ) ){
- //add clique lemma
- addCliqueLemma( clique, out );
- return;
- }
- }else{
- int sp = addSplit( d_regions[i], out );
- if( sp==1 ){
- addedLemma = true;
+
+ int sp = addSplit( d_regions[i], out );
+ if( sp==1 ){
+ addedLemma = true;
#ifdef ONE_SPLIT_REGION
- break;
+ break;
#endif
- }else if( sp==-1 ){
- check( level, out );
- return;
- }
+ }else if( sp==-1 ){
+ check( level, out );
+ return;
}
}
}
return Node::null();
}
-bool SortModel::minimize( OutputChannel* out, TheoryModel* m ){
- if( options::ufssTotality() ){
- //do nothing
- }else{
- if( m ){
-#if 0
- // ensure that the constructed model is minimal
- // if the model has terms that the strong solver does not know about
- if( (int)rs->d_type_reps[ d_type ].size()>d_cardinality ){
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->getEqualityEngine() );
- while( !eqcs_i.isFinished() ){
- Node eqc = (*eqcs_i);
- if( eqc.getType()==d_type ){
- //we must ensure that this equivalence class has been accounted for
- if( d_regions_map.find( eqc )==d_regions_map.end() ){
- //split on unaccounted for term and cardinality lemma term (as default)
- Node splitEq = eqc.eqNode( d_cardinality_term );
- splitEq = Rewriter::rewrite( splitEq );
- Trace("uf-ss-minimize") << "Last chance minimize : " << splitEq << std::endl;
- out->split( splitEq );
- //tell the sat solver to explore the equals branch first
- out->requirePhase( splitEq, true );
- ++( d_thss->d_statistics.d_split_lemmas );
- return false;
- }
- }
- ++eqcs_i;
- }
- Assert( false );
- }
-#endif
- }else{
- Trace("uf-ss-debug") << "Minimize the UF model..." << std::endl;
- //internal minimize, ensure that model forms a clique:
- // if two equivalence classes are neither equal nor disequal, add a split
- int validRegionIndex = -1;
- for( int i=0; i<(int)d_regions_index; i++ ){
- if( d_regions[i]->valid() ){
- if( validRegionIndex!=-1 ){
- combineRegions( validRegionIndex, i );
- if( addSplit( d_regions[validRegionIndex], out )!=0 ){
- Trace("uf-ss-debug") << "Minimize model : combined regions, found split. " << std::endl;
- return false;
- }
- }else{
- validRegionIndex = i;
- }
- }
- }
- Assert( validRegionIndex!=-1 );
- if( addSplit( d_regions[validRegionIndex], out )!=0 ){
- Trace("uf-ss-debug") << "Minimize model : found split. " << std::endl;
- return false;
- }
- Trace("uf-ss-debug") << "Minimize success. " << std::endl;
- }
- }
- return true;
-}
-
-
int SortModel::getNumDisequalitiesToRegion( Node n, int ri ){
int ni = d_regions_map[n];
int counter = 0;
}
}
}else{
- /*
- if( options::ufssModelInference() ){
- //check if we are at decision level 0
- if( d_th->d_valuation.getAssertionLevel()==0 ){
- Trace("uf-ss-mi") << "We have proved that no models of size " << c << " for type " << d_type << " exist." << std::endl;
- Trace("uf-ss-mi") << " # Clique lemmas : " << d_cliques[c].size() << std::endl;
- if( d_cliques[c].size()==1 ){
- if( d_totality_terms[c+1].empty() ){
- Trace("uf-ss-mi") << "*** Establish model" << std::endl;
- //d_totality_terms[c+1].insert( d_totality_terms[c].begin(), d_cliques[c][0].begin(), d_cliques[c][0].end() );
- }
- }
- }
- }
- */
//see if we need to request a new cardinality
if( !d_hasCard ){
bool needsCard = true;
while( clique.size()>size_t(d_cardinality+1) ){
clique.pop_back();
}
- //debugging information
- if( Trace.isOn("uf-ss-cliques") ){
- std::vector< Node > clique_vec;
- clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() );
- addClique( d_cardinality, clique_vec );
- }
// add as lemma
std::vector<Node> eqs;
for (unsigned i = 0, size = clique.size(); i < size; i++)
}
}
-void SortModel::addClique( int c, std::vector< Node >& clique ) {
- //if( d_clique_trie[c].add( clique ) ){
- // d_cliques[ c ].push_back( clique );
- //}
-}
-
-
/** apply totality */
bool SortModel::applyTotality( int cardinality ){
return options::ufssTotality() || cardinality<=options::ufssTotalityLimited();
- // || ( options::ufssModelInference() && !d_totality_terms[cardinality].empty() );
}
/** get totality lemma terms */
Node SortModel::getTotalityLemmaTerm( int cardinality, int i ){
return d_totality_terms[0][i];
- //}else{
- // return d_totality_terms[cardinality][i];
- //}
}
void SortModel::simpleCheckCardinality() {
}
}
-void StrongSolverTheoryUF::notifyRestart(){}
-
/** get cardinality for sort */
int StrongSolverTheoryUF::getCardinality( Node n ) {
SortModel* c = getSortModel( n );
return -1;
}
-bool StrongSolverTheoryUF::minimize( TheoryModel* m ){
- for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
- if( !it->second->minimize( d_out, m ) ){
- return false;
- }
- }
- for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
- Trace("uf-ss-minimize") << "Cardinality( " << it->first << " ) : " << it->second->getCardinality() << std::endl;
- }
- return true;
-}
-
//print debug
void StrongSolverTheoryUF::debugPrint( const char* c ){
//EqClassesIterator< TheoryUF::NotifyClass > eqc_iter( &((TheoryUF*)d_th)->d_equalityEngine );
void getNumExternalDisequalities(std::map< Node, int >& num_ext_disequalities );
/** check for cliques */
bool check( Theory::Effort level, int cardinality, std::vector< Node >& clique );
- /** get candidate clique */
- bool getCandidateClique( int cardinality, std::vector< Node >& clique );
//print debug
void debugPrint( const char* c, bool incClique = false );
void addCliqueLemma( std::vector< Node >& clique, OutputChannel* out );
/** add totality axiom */
void addTotalityAxiom( Node n, int cardinality, OutputChannel* out );
-
- class NodeTrie {
- public:
- bool add( std::vector< Node >& n, unsigned i = 0 ){
- Assert( i<n.size() );
- if( i==(n.size()-1) ){
- bool ret = d_children.find( n[i] )==d_children.end();
- d_children[n[i]].d_children.clear();
- return ret;
- }else{
- return d_children[n[i]].add( n, i+1 );
- }
- }
- private:
- std::map< Node, NodeTrie > d_children;
- }; /* class NodeTrie */
-
- std::map< int, NodeTrie > d_clique_trie;
- void addClique( int c, std::vector< Node >& clique );
-
/** Are we in conflict */
context::CDO<bool> d_conflict;
/** cardinality */
void propagate( Theory::Effort level, OutputChannel* out );
/** get next decision request */
Node getNextDecisionRequest();
- /** minimize */
- bool minimize( OutputChannel* out, TheoryModel* m );
/** assert cardinality */
void assertCardinality( OutputChannel* out, int c, bool val );
/** is in conflict */
Node getNextDecisionRequest( unsigned& priority );
/** preregister a term */
void preRegisterTerm( TNode n );
- /** notify restart */
- void notifyRestart();
/** identify */
std::string identify() const { return std::string("StrongSolverTheoryUF"); }
//print debug
int getCardinality( Node n );
/** get cardinality for type */
int getCardinality( TypeNode tn );
- /** minimize */
- bool minimize( TheoryModel* m = NULL );
/** has eqc */
bool hasEqc(Node a);
projects / cvc5.git / commitdiff