}
# designed for 300 seconds
-trywith 20 --relevant-triggers --full-saturate-quant
+trywith 20 --relational-triggers --full-saturate-quant
trywith 20 --no-e-matching --full-saturate-quant
-trywith 20 --finite-model-find --mbqi=abs
+trywith 15 --finite-model-find --mbqi=abs
trywith 5 --multi-trigger-when-single --full-saturate-quant
trywith 5 --trigger-sel=max --full-saturate-quant
-trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant
-trywith 5 --relational-triggers --full-saturate-quant
-trywith 15 --term-db-mode=relevant --full-saturate-quant
-trywith 15 --pre-quant=none --full-saturate-quant
-trywith 15 --finite-model-find --uf-ss=no-minimal
-trywith 30 --decision=internal --full-saturate-quant
+trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant
+trywith 10 --finite-model-find --uf-ss=no-minimal --sort-inference --uf-ss-fair
+trywith 10 --term-db-mode=relevant --full-saturate-quant
+trywith 15 --prenex-quant=none --full-saturate-quant
+trywith 15 --decision=internal --full-saturate-quant
+trywith 30 --relevant-triggers --full-saturate-quant
+trywith 30 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair
trywith 30 --fs-inst --full-saturate-quant
trywith 30 --no-quant-cf --full-saturate-quant
-finishwith --relational-triggers --full-saturate-quant
+finishwith --qcf-vo-exp --full-saturate-quant
# echo "% SZS status" "GaveUp for $filename"
trywith 10 --decision=internal --full-saturate-quant
trywith 10 --finite-model-find --decision=internal
-trywith 10 ---purify-quant --full-saturate-quant
-trywith 10 ---partial-triggers --full-saturate-quant
-trywith 10 ---no-e-matching --full-saturate-quant
+trywith 10 --purify-quant --full-saturate-quant
+trywith 10 --partial-triggers --full-saturate-quant
+trywith 10 --no-e-matching --full-saturate-quant
trywith 30 --cbqi-all --purify-triggers --full-saturate-quant
-trywith 60 --cbqi-all ---fs-inst --full-saturate-quant
+trywith 60 --cbqi-all --fs-inst --full-saturate-quant
finishwith --full-saturate-quant
# echo "% SZS status" "GaveUp for $filename"
+ Enforce fairness using an uninterpreted function for datatypes size.\n\
\n\
default | dt-size \n\
-+ Default, enforce fairness using size theory operator.\n\
++ Default, enforce fairness using size operator.\n\
\n\
dt-height-bound \n\
+ Enforce fairness by height bound predicate.\n\
return theory::quantifiers::CEGQI_FAIR_DT_SIZE;
} else if(optarg == "dt-height-bound" ){
return theory::quantifiers::CEGQI_FAIR_DT_HEIGHT_PRED;
+ //} else if(optarg == "dt-size-bound" ){
+ // return theory::quantifiers::CEGQI_FAIR_DT_SIZE_PRED;
} else if(optarg == "none") {
return theory::quantifiers::CEGQI_FAIR_NONE;
} else if(optarg == "help") {
CEGQI_FAIR_DT_SIZE,
/** enforce fairness by datatypes height bound */
CEGQI_FAIR_DT_HEIGHT_PRED,
+ /** enforce fairness by datatypes size bound */
+ CEGQI_FAIR_DT_SIZE_PRED,
/** do not use fair strategy for CEGQI */
CEGQI_FAIR_NONE,
};
option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false
only add instantiations for one quantifier per round for mbqi
-option fmfInstEngine --fmf-inst-engine bool :default false
+option fmfInstEngine --fmf-inst-engine bool :default false :read-write
use instantiation engine in conjunction with finite model finding
option fmfInstGen --fmf-inst-gen bool :default true
enable Inst-Gen instantiation techniques for finite model finding
option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToSygusInvTemplMode
template mode for sygus invariant synthesis
-option sygusEagerUnfold --sygus-eager-unfold bool :default false
- eager unfold evaluation functions
+option sygusDirectEval --sygus-direct-eval bool :default false
+ direct unfolding of evaluation functions
# approach applied to general quantified formulas
option cbqiSplx --cbqi-splx bool :read-write :default false
//since we enforce satisfaction completeness, immediately convert to total version
if( k==CVC4::kind::BITVECTOR_UDIV ){
k = CVC4::kind::BITVECTOR_UDIV_TOTAL;
+ }else if( k==CVC4::kind::BITVECTOR_UREM ){
+ k = CVC4::kind::BITVECTOR_UREM_TOTAL;
}
sgt.d_name = kind::kindToString(k);
sgt.d_gterm_type = SygusGTerm::gterm_op;
k = PARSER_STATE->getOperatorKind(name);
if( k==CVC4::kind::BITVECTOR_UDIV ){
k = CVC4::kind::BITVECTOR_UDIV_TOTAL;
+ }else if( k==CVC4::kind::BITVECTOR_UREM ){
+ k = CVC4::kind::BITVECTOR_UREM_TOTAL;
}
sgt.d_name = kind::kindToString(k);
sgt.d_gterm_type = SygusGTerm::gterm_op;
options::fmfBoundInt.set( true );
Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
}
+ if(! options::fmfInstEngine.wasSetByUser()) {
+ options::fmfInstEngine.set( true );
+ Trace("smt") << "turning on fmf-inst-engine, for strings-exp" << std::endl;
+ }
/*
if(! options::rewriteDivk.wasSetByUser()) {
options::rewriteDivk.set( true );
Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
-
dumpAssertions("pre-constrain-subtypes", d_assertions);
{
// Any variables of subtype types need to be constrained properly.
operator DT_SIZE 1 "datatypes size"
typerule DT_SIZE ::CVC4::theory::datatypes::DtSizeTypeRule
-operator DT_HEIGHT_BOUND 1 "datatypes height bound"
+operator DT_HEIGHT_BOUND 2 "datatypes height bound"
typerule DT_HEIGHT_BOUND ::CVC4::theory::datatypes::DtHeightBoundTypeRule
endtheory
throw TypeCheckingExceptionPrivate(n, "datatype height bound must be non-negative");
}
}
- return nodeManager->integerType();
+ return nodeManager->booleanType();
}
};/* class DtHeightBoundTypeRule */
-
}/* CVC4::theory::datatypes namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
qe->getOutputChannel().lemma( lem );
qe->getOutputChannel().requirePhase( lit, true );
- if( getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED ){
+ if( getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED || getCegqiFairMode()==CEGQI_FAIR_DT_SIZE_PRED ){
//implies height bounds on each candidate variable
std::vector< Node > lem_c;
for( unsigned j=0; j<d_candidates.size(); j++ ){
- lem_c.push_back( NodeManager::currentNM()->mkNode( DT_HEIGHT_BOUND, d_candidates[j], c ) );
+ if( getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED ){
+ lem_c.push_back( NodeManager::currentNM()->mkNode( DT_HEIGHT_BOUND, d_candidates[j], c ) );
+ }else{
+ //lem_c.push_back( NodeManager::currentNM()->mkNode( DT_SIZE_BOUND, d_candidates[j], c ) );
+ }
}
Node hlem = NodeManager::currentNM()->mkNode( OR, lit.negate(), lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c ) );
- Trace("cegqi-lemma") << "Cegqi::Lemma : Fairness expansion (dt-height-pred) : " << hlem << std::endl;
+ Trace("cegqi-lemma") << "Cegqi::Lemma : Fairness expansion (pred) : " << hlem << std::endl;
qe->getOutputChannel().lemma( hlem );
}
return lit;
}
}
+void CegInstantiation::preRegisterQuantifier( Node q ) {
+ if( options::sygusDirectEval() ){
+ if( q.getNumChildren()==3 && q[2].getKind()==INST_PATTERN_LIST && q[2][0].getKind()==INST_PATTERN ){
+ //check whether it is an evaluation axiom
+ Node pat = q[2][0][0];
+ if( pat.getKind()==APPLY_UF ){
+ TypeNode tn = pat[0].getType();
+ if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ if( dt.isSygus() ){
+ //take ownership of this quantified formula (will use direct evaluation instead of instantiation)
+ d_quantEngine->setOwner( q, this );
+ d_eval_axioms[q] = true;
+ }
+ }
+ }
+ }
+ }
+}
+
void CegInstantiation::registerQuantifier( Node q ) {
- if( d_quantEngine->getOwner( q )==this ){
+ if( d_quantEngine->getOwner( q )==this && d_eval_axioms.find( q )==d_eval_axioms.end() ){
if( !d_conj->isAssigned() ){
Trace("cegqi") << "Register conjecture : " << q << std::endl;
d_conj->assign( q );
if( it!=d_uf_measure.end() ){
mc.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, it->second, d_conj->d_candidates[j] ) );
}
- }else if( d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED ){
+ }else if( d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED || d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_SIZE_PRED ){
//measure term is a fresh constant
mc.push_back( NodeManager::currentNM()->mkSkolem( "K", NodeManager::currentNM()->integerType() ) );
}
Trace("cegqi-engine-debug") << conj->d_candidates[i] << " ";
}
Trace("cegqi-engine-debug") << std::endl;
+ Trace("cegqi-engine-debug") << " * Candidate ce skolems : ";
+ for( unsigned i=0; i<conj->d_ce_sk.size(); i++ ){
+ Trace("cegqi-engine-debug") << conj->d_ce_sk[i] << " ";
+ }
+ Trace("cegqi-engine-debug") << std::endl;
if( conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){
Trace("cegqi-engine") << " * Current term size : " << conj->d_curr_lit.get() << std::endl;
}
}
std::vector< Node > model_values;
if( getModelValues( conj, conj->d_candidates, model_values ) ){
+ if( options::sygusDirectEval() ){
+ std::vector< Node > eager_eval_lem;
+ for( unsigned j=0; j<conj->d_candidates.size(); j++ ){
+ d_quantEngine->getTermDatabaseSygus()->registerModelValue( conj->d_candidates[j], model_values[j], eager_eval_lem );
+ }
+ if( !eager_eval_lem.empty() ){
+ for( unsigned j=0; j<eager_eval_lem.size(); j++ ){
+ Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << eager_eval_lem[j] << std::endl;
+ d_quantEngine->addLemma( eager_eval_lem[j] );
+ }
+ return;
+ }
+ }
//check if we must apply fairness lemmas
if( conj->getCegqiFairMode()==CEGQI_FAIR_UF_DT_SIZE ){
std::vector< Node > lems;
Node lem = NodeManager::currentNM()->mkNode( OR, ic );
lem = Rewriter::rewrite( lem );
d_last_inst_si = false;
+ //eagerly unfold applications of evaluation function
+ if( options::sygusDirectEval() ){
+ Trace("cegqi-eager") << "pre-unfold counterexample : " << lem << std::endl;
+ std::map< Node, Node > visited_n;
+ lem = getEagerUnfold( lem, visited_n );
+ }
+
Trace("cegqi-lemma") << "Cegqi::Lemma : counterexample : " << lem << std::endl;
- d_quantEngine->addLemma( lem );
- ++(d_statistics.d_cegqi_lemmas_ce);
- Trace("cegqi-engine") << " ...find counterexample." << std::endl;
- //optimization : eagerly unfold applications of evaluation function
- if( options::sygusEagerUnfold() ){
- std::vector< Node > eager_lems;
- std::map< Node, bool > visited;
- getEagerUnfoldLemmas( eager_lems, lem, visited );
- for( unsigned i=0; i<eager_lems.size(); i++ ){
- Trace("cegqi-lemma") << "Cegqi::Lemma : eager unfold : " << eager_lems[i] << std::endl;
- d_quantEngine->addLemma( eager_lems[i] );
+ if( d_quantEngine->addLemma( lem ) ){
+ ++(d_statistics.d_cegqi_lemmas_ce);
+ Trace("cegqi-engine") << " ...find counterexample." << std::endl;
+ }else{
+ //this may happen if we eagerly unfold, simplify to true
+ if( !options::sygusDirectEval() ){
+ Trace("cegqi-engine") << " ...FAILED to add candidate!" << std::endl;
+ }else{
+ Trace("cegqi-engine-debug") << " ...FAILED to add candidate!" << std::endl;
+ }
+ if( conj->d_refine_count==0 ){
+ //immediately go to refine candidate
+ checkCegConjecture( conj );
+ return;
}
}
}
}
}
-void CegInstantiation::getEagerUnfoldLemmas( std::vector< Node >& lems, Node n, std::map< Node, bool >& visited ) {
- if( visited.find( n )==visited.end() ){
- Trace("cegqi-eager-debug") << "getEagerUnfoldLemmas " << n << std::endl;
- visited[n] = true;
+Node CegInstantiation::getEagerUnfold( Node n, std::map< Node, Node >& visited ) {
+ std::map< Node, Node >::iterator itv = visited.find( n );
+ if( itv==visited.end() ){
+ Trace("cegqi-eager-debug") << "getEagerUnfold " << n << std::endl;
+ Node ret;
if( n.getKind()==APPLY_UF ){
TypeNode tn = n[0].getType();
Trace("cegqi-eager-debug") << "check " << n[0].getType() << std::endl;
if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- if( dt.isSygus() ){
+ if( dt.isSygus() ){
Trace("cegqi-eager") << "Unfold eager : " << n << std::endl;
Node bTerm = d_quantEngine->getTermDatabaseSygus()->sygusToBuiltin( n[0], tn );
Trace("cegqi-eager") << "Built-in term : " << bTerm << std::endl;
vars.push_back( var_list[j] );
}
for( unsigned j=1; j<n.getNumChildren(); j++ ){
+ Node nc = getEagerUnfold( n[j], visited );
if( var_list[j-1].getType().isBoolean() ){
//TODO: remove this case when boolean term conversion is eliminated
Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
- subs.push_back( n[j].eqNode( c ) );
+ subs.push_back( nc.eqNode( c ) );
}else{
- subs.push_back( n[j] );
+ subs.push_back( nc );
}
Assert( subs[j-1].getType()==var_list[j-1].getType() );
}
Trace("cegqi-eager") << "Built-in term after subs : " << bTerm << std::endl;
Trace("cegqi-eager-debug") << "Types : " << bTerm.getType() << " " << n.getType() << std::endl;
Assert( n.getType()==bTerm.getType() );
- Node lem = Rewriter::rewrite( NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, n, bTerm ) );
- lems.push_back( lem );
+ ret = bTerm;
}
}
}
- if( n.getKind()!=FORALL ){
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- getEagerUnfoldLemmas( lems, n[i], visited );
+ if( ret.isNull() ){
+ if( n.getKind()!=FORALL ){
+ bool childChanged = false;
+ std::vector< Node > children;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ Node nc = getEagerUnfold( n[i], visited );
+ childChanged = childChanged || n[i]!=nc;
+ children.push_back( nc );
+ }
+ if( childChanged ){
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.insert( children.begin(), n.getOperator() );
+ }
+ ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+ }
+ }
+ if( ret.isNull() ){
+ ret = n;
}
}
+ visited[n] = ret;
+ return ret;
+ }else{
+ return itv->second;
}
}
CegConjecture * d_conj;
/** last instantiation by single invocation module? */
bool d_last_inst_si;
+ /** evaluation axioms */
+ std::map< Node, bool > d_eval_axioms;
private: //for enforcing fairness
/** measure functions */
std::map< TypeNode, Node > d_uf_measure;
/** get measure lemmas */
void getMeasureLemmas( Node n, Node v, std::vector< Node >& lems );
/** get eager unfolding */
- void getEagerUnfoldLemmas( std::vector< Node >& lems, Node n, std::map< Node, bool >& visited );
+ Node getEagerUnfold( Node n, std::map< Node, Node >& visited );
private:
/** check conjecture */
void checkCegConjecture( CegConjecture * conj );
/* Call during quantifier engine's check */
void check( Theory::Effort e, unsigned quant_e );
/* Called for new quantifiers */
+ void preRegisterQuantifier( Node q );
void registerQuantifier( Node q );
void assertNode( Node n );
Node getNextDecisionRequest();
void InstStrategyCegqi::registerQuantifier( Node q ) {
if( options::cbqiPreRegInst() ){
- //just get the instantiator
- getInstantiator( q );
+ if( doCbqi( q ) ){
+ //just get the instantiator
+ getInstantiator( q );
+ }
}
}
if( n.getKind()==BOUND_VARIABLE ){
d_inMatchConstraint[n] = true;
}
- //if( MatchGen::isHandledUfTerm( n ) || n.getKind()==ITE ){
if( d_var_num.find( n )==d_var_num.end() ){
Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl;
d_var_num[n] = d_vars.size();
if( isVar ){
Assert( qi->d_var_num.find( n )!=qi->d_var_num.end() );
if( n.getKind()==ITE ){
- /*
- d_type = typ_ite_var;
- d_type_not = false;
- d_n = n;
- d_children.push_back( MatchGen( qi, d_n[0] ) );
- if( d_children[0].isValid() ){
- d_type = typ_ite_var;
- for( unsigned i=1; i<=2; i++ ){
- Node nn = n.eqNode( n[i] );
- d_children.push_back( MatchGen( qi, nn ) );
- d_children[d_children.size()-1].d_qni_bound_except.push_back( 0 );
- if( !d_children[d_children.size()-1].isValid() ){
- setInvalid();
- break;
- }
- }
- }else{
-*/
- d_type = typ_invalid;
- //}
+ d_type = typ_invalid;
}else{
d_type = isHandledUfTerm( n ) ? typ_var : typ_tsym;
d_qni_var_num[0] = qi->getVarNum( n );
break;
}
}
- /*
- else if( isTop && n.getKind()==OR && d_children[d_children.size()-1].d_type==typ_var_eq ){
- Trace("qcf-qregister-debug") << "Remove child, make built-in constraint" << std::endl;
- //if variable equality/disequality at top level, remove immediately
- bool cIsNot = d_children[d_children.size()-1].d_type_not;
- Node cn = d_children[d_children.size()-1].d_n;
- Assert( cn.getKind()==EQUAL );
- Assert( p->d_qinfo[q].isVar( cn[0] ) || p->d_qinfo[q].isVar( cn[1] ) );
- //make it a built-in constraint instead
- for( unsigned i=0; i<2; i++ ){
- if( p->d_qinfo[q].isVar( cn[i] ) ){
- int v = p->d_qinfo[q].getVarNum( cn[i] );
- Node cno = cn[i==0 ? 1 : 0];
- p->d_qinfo[q].d_var_constraint[ cIsNot ? 0 : 1 ][v].push_back( cno );
- break;
- }
- }
- d_children.pop_back();
- }
- */
}
}else{
d_type = typ_invalid;
d_type = typ_ground;
qi->setGroundSubterm( d_n );
}
- //if( d_type!=typ_invalid ){
- //determine an efficient children ordering
- //if( !d_children.empty() ){
- //for( unsigned i=0; i<d_children.size(); i++ ){
- // d_children_order.push_back( i );
- //}
- //if( !d_n.isNull() && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF ) ){
- //sort based on the type of the constraint : ground comes first, then literals, then others
- //MatchGenSort mgs;
- //mgs.d_mg = this;
- //std::sort( d_children_order.begin(), d_children_order.end(), mgs );
- //}
- //}
- //}
}
Trace("qcf-qregister-debug") << "Done make match gen " << n << ", type = ";
debugPrintType( "qcf-qregister-debug", d_type, true );
//add to children order
d_children_order.push_back( min_score_index );
assigned[min_score_index] = true;
- //if( vb_count[min_score_index]==0 ){
- // d_independent.push_back( min_score_index );
- //}
//determine order internal to children
d_children[min_score_index].determineVariableOrder( qi, bvars );
Trace("qcf-qregister-debug") << "...bind variables" << std::endl;
//now, make it a bound variable
- for( unsigned i=0; i<c_to_vars[min_score_index].size(); i++ ){
- int v = c_to_vars[min_score_index][i];
- if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){
- for( unsigned j=0; j<vars_to_c[v].size(); j++ ){
- int vc = vars_to_c[v][j];
- vu_count[vc]--;
- vb_count[vc]++;
+ if( vu_count[min_score_index]>0 ){
+ for( unsigned i=0; i<c_to_vars[min_score_index].size(); i++ ){
+ int v = c_to_vars[min_score_index][i];
+ if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){
+ for( unsigned j=0; j<vars_to_c[v].size(); j++ ){
+ int vc = vars_to_c[v][j];
+ vu_count[vc]--;
+ vb_count[vc]++;
+ }
+ bvars.push_back( v );
}
- bvars.push_back( v );
}
}
Trace("qcf-qregister-debug") << "...done assign child " << min_score_index << std::endl;
}
bool MatchGen::isHandledBoolConnective( TNode n ) {
- return n.getType().isBoolean() && TermDb::isBoolConnective( n.getKind() );
+ return TermDb::isBoolConnective( n.getKind() ) && ( n.getKind()!=ITE || n.getType().isBoolean() );
}
bool MatchGen::isHandledUfTerm( TNode n ) {
if( d_quantEngine->hasOwnership( q, this ) ){
d_quants.push_back( q );
d_quant_id[q] = d_quants.size();
- Trace("qcf-qregister") << "Register ";
- debugPrintQuant( "qcf-qregister", q );
- Trace("qcf-qregister") << " : " << q << std::endl;
+ if( Trace.isOn("qcf-qregister") ){
+ Trace("qcf-qregister") << "Register ";
+ debugPrintQuant( "qcf-qregister", q );
+ Trace("qcf-qregister") << " : " << q << std::endl;
+ }
//make QcfNode structure
Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;
d_qinfo[q].initialize( this, q, q[1] );
//debug print
- Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;
- Trace("qcf-qregister") << " ";
- debugPrintQuantBody( "qcf-qregister", q, q[1] );
- Trace("qcf-qregister") << std::endl;
- if( d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){
- Trace("qcf-qregister") << " with additional constraints : " << std::endl;
- for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){
- Trace("qcf-qregister") << " ?x" << j << " = ";
- debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false );
- Trace("qcf-qregister") << std::endl;
- }
- }
-
- Trace("qcf-qregister") << "Done registering quantifier." << std::endl;
+ if( Trace.isOn("qcf-qregister") ){
+ Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;
+ Trace("qcf-qregister") << " ";
+ debugPrintQuantBody( "qcf-qregister", q, q[1] );
+ Trace("qcf-qregister") << std::endl;
+ if( d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){
+ Trace("qcf-qregister") << " with additional constraints : " << std::endl;
+ for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){
+ Trace("qcf-qregister") << " ?x" << j << " = ";
+ debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false );
+ Trace("qcf-qregister") << std::endl;
+ }
+ }
+ Trace("qcf-qregister") << "Done registering quantifier." << std::endl;
+ }
}
}
d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
if( options::ceGuidedInst() ){
- d_sygus_tdb = new TermDbSygus;
+ d_sygus_tdb = new TermDbSygus( c, qe );
}else{
d_sygus_tdb = NULL;
}
Node op = getMatchOperator( n );
d_op_map[op].push_back( n );
added.insert( n );
+
+ if( d_sygus_tdb ){
+ d_sygus_tdb->registerEvalTerm( n );
+ }
if( options::eagerInstQuant() ){
for( unsigned i=0; i<n.getNumChildren(); i++ ){
return qy->getEngine()->getRepresentative( n1 ) == ( pol ? d_true : d_false );
}
}
- }else if( n.getKind()==FORALL ){
+ }else if( n.getKind()==FORALL && !pol ){
return isEntailed2( n[1], subs, subsRep, hasSubs, pol, qy );
}
return false;
//this function makes a canonical representation of a term (
// - orders variables left to right
// - if apply_torder, then sort direct subterms of commutative operators
-Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder ) {
+Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder, std::map< TNode, Node >& visited ) {
Trace("canon-term-debug") << "Get canonical term for " << n << std::endl;
if( n.getKind()==BOUND_VARIABLE ){
std::map< TNode, TNode >::iterator it = subs.find( n );
return it->second;
}
}else if( n.getNumChildren()>0 ){
- //collect children
- Trace("canon-term-debug") << "Collect children" << std::endl;
- std::vector< Node > cchildren;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- cchildren.push_back( n[i] );
- }
- //if applicable, first sort by term order
- if( apply_torder && isComm( n.getKind() ) ){
- Trace("canon-term-debug") << "Sort based on commutative operator " << n.getKind() << std::endl;
- sortTermOrder sto;
- sto.d_tdb = this;
- std::sort( cchildren.begin(), cchildren.end(), sto );
- }
- //now make canonical
- Trace("canon-term-debug") << "Make canonical children" << std::endl;
- for( unsigned i=0; i<cchildren.size(); i++ ){
- cchildren[i] = getCanonicalTerm( cchildren[i], var_count, subs, apply_torder );
- }
- if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
- Trace("canon-term-debug") << "Insert operator " << n.getOperator() << std::endl;
- cchildren.insert( cchildren.begin(), n.getOperator() );
- }
- Trace("canon-term-debug") << "...constructing for " << n << "." << std::endl;
- Node ret = NodeManager::currentNM()->mkNode( n.getKind(), cchildren );
- Trace("canon-term-debug") << "...constructed " << ret << " for " << n << "." << std::endl;
- return ret;
+ std::map< TNode, Node >::iterator it = visited.find( n );
+ if( it!=visited.end() ){
+ return it->second;
+ }else{
+ //collect children
+ Trace("canon-term-debug") << "Collect children" << std::endl;
+ std::vector< Node > cchildren;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ cchildren.push_back( n[i] );
+ }
+ //if applicable, first sort by term order
+ if( apply_torder && isComm( n.getKind() ) ){
+ Trace("canon-term-debug") << "Sort based on commutative operator " << n.getKind() << std::endl;
+ sortTermOrder sto;
+ sto.d_tdb = this;
+ std::sort( cchildren.begin(), cchildren.end(), sto );
+ }
+ //now make canonical
+ Trace("canon-term-debug") << "Make canonical children" << std::endl;
+ for( unsigned i=0; i<cchildren.size(); i++ ){
+ cchildren[i] = getCanonicalTerm( cchildren[i], var_count, subs, apply_torder, visited );
+ }
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ Trace("canon-term-debug") << "Insert operator " << n.getOperator() << std::endl;
+ cchildren.insert( cchildren.begin(), n.getOperator() );
+ }
+ Trace("canon-term-debug") << "...constructing for " << n << "." << std::endl;
+ Node ret = NodeManager::currentNM()->mkNode( n.getKind(), cchildren );
+ Trace("canon-term-debug") << "...constructed " << ret << " for " << n << "." << std::endl;
+ visited[n] = ret;
+ return ret;
+ }
}else{
Trace("canon-term-debug") << "...return 0-child term." << std::endl;
return n;
Node TermDb::getCanonicalTerm( TNode n, bool apply_torder ){
std::map< TypeNode, unsigned > var_count;
std::map< TNode, TNode > subs;
- return getCanonicalTerm( n, var_count, subs, apply_torder );
+ std::map< TNode, Node > visited;
+ return getCanonicalTerm( n, var_count, subs, apply_torder, visited );
}
void TermDb::getVtsTerms( std::vector< Node >& t, bool isFree, bool create, bool inc_delta ) {
}
}
-TermDbSygus::TermDbSygus(){
+TermDbSygus::TermDbSygus( context::Context* c, QuantifiersEngine* qe ) : d_quantEngine( qe ){
d_true = NodeManager::currentNM()->mkConst( true );
d_false = NodeManager::currentNM()->mkConst( false );
}
+bool TermDbSygus::reset( Theory::Effort e ) {
+ return true;
+}
+
TNode TermDbSygus::getVar( TypeNode tn, int i ) {
while( i>=(int)d_fv[tn].size() ){
std::stringstream ss;
out << n;
}
}
+
+void TermDbSygus::registerEvalTerm( Node n ) {
+ if( options::sygusDirectEval() ){
+ if( n.getKind()==APPLY_UF ){
+ Trace("sygus-eager") << "TermDbSygus::eager: Register eval term : " << n << std::endl;
+ TypeNode tn = n[0].getType();
+ if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ if( dt.isSygus() ){
+ Node f = n.getOperator();
+ Trace("sygus-eager") << "...the evaluation function is : " << f << std::endl;
+ Assert( n[0].getKind()!=APPLY_CONSTRUCTOR );
+ d_evals[n[0]].push_back( n );
+ TypeNode tn = n[0].getType();
+ Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ Node var_list = Node::fromExpr( dt.getSygusVarList() );
+ Assert( dt.isSygus() );
+ d_eval_args[n[0]].push_back( std::vector< Node >() );
+ for( unsigned j=1; j<n.getNumChildren(); j++ ){
+ if( var_list[j-1].getType().isBoolean() ){
+ //TODO: remove this case when boolean term conversion is eliminated
+ Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
+ d_eval_args[n[0]].back().push_back( n[j].eqNode( c ) );
+ }else{
+ d_eval_args[n[0]].back().push_back( n[j] );
+ }
+ }
+
+ }
+ }
+ }
+ }
+}
+
+void TermDbSygus::registerModelValue( Node n, Node v, std::vector< Node >& lems ) {
+ std::map< Node, std::vector< std::vector< Node > > >::iterator it = d_eval_args.find( n );
+ if( it!=d_eval_args.end() && !it->second.empty() ){
+ unsigned start = d_node_mv_args_proc[n][v];
+ Node antec = n.eqNode( v ).negate();
+ TypeNode tn = n.getType();
+ Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ Assert( dt.isSygus() );
+ Trace("sygus-eager") << "TermDbSygus::eager: Register model value : " << v << " for " << n << std::endl;
+ Trace("sygus-eager") << "...it has " << it->second.size() << " evaluations, already processed " << start << "." << std::endl;
+ Node bTerm = d_quantEngine->getTermDatabaseSygus()->sygusToBuiltin( v, tn );
+ Trace("sygus-eager") << "Built-in term : " << bTerm << std::endl;
+ std::vector< Node > vars;
+ Node var_list = Node::fromExpr( dt.getSygusVarList() );
+ for( unsigned j=0; j<var_list.getNumChildren(); j++ ){
+ vars.push_back( var_list[j] );
+ }
+ //for each evaluation
+ for( unsigned i=start; i<it->second.size(); i++ ){
+ Assert( vars.size()==it->second[i].size() );
+ Node sBTerm = bTerm.substitute( vars.begin(), vars.end(), it->second[i].begin(), it->second[i].end() );
+ Node lem = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, d_evals[n][i], sBTerm );
+ lem = NodeManager::currentNM()->mkNode( OR, antec, lem );
+ Trace("sygus-eager") << "Lemma : " << lem << std::endl;
+ lems.push_back( lem );
+ }
+ d_node_mv_args_proc[n][v] = it->second.size();
+ }
+}
+
//free variables
std::map< TypeNode, std::vector< Node > > d_cn_free_var;
// get canonical term, return null if it contains a term apart from handled signature
- Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder );
+ Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder,
+ std::map< TNode, Node >& visited );
public:
/** get id for operator */
int getIdForOperator( Node op );
class TermDbSygus {
private:
+ /** reference to the quantifiers engine */
+ QuantifiersEngine* d_quantEngine;
std::map< TypeNode, std::vector< Node > > d_fv;
std::map< Node, TypeNode > d_fv_stype;
std::map< Node, int > d_fv_num;
std::map< TypeNode, std::map< Node, Node > > d_sygus_to_builtin;
std::map< TypeNode, std::map< Node, Node > > d_builtin_const_to_sygus;
public:
- TermDbSygus();
+ TermDbSygus( context::Context* c, QuantifiersEngine* qe );
+ ~TermDbSygus(){}
+ bool reset( Theory::Effort e );
+ std::string identify() const { return "TermDbSygus"; }
+
bool isRegistered( TypeNode tn );
TypeNode sygusToBuiltinType( TypeNode tn );
int getKindArg( TypeNode tn, Kind k );
static Kind getOperatorKind( Node op );
/** print sygus term */
static void printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs );
+
+//for eager instantiation
+private:
+ std::map< Node, std::vector< Node > > d_evals;
+ std::map< Node, std::vector< std::vector< Node > > > d_eval_args;
+ std::map< Node, std::map< Node, unsigned > > d_node_mv_args_proc;
+public:
+ void registerEvalTerm( Node n );
+ void registerModelValue( Node n, Node v, std::vector< Node >& lems );
};
}/* CVC4::theory::quantifiers namespace */
void TheoryQuantifiers::preRegisterTerm(TNode n) {
Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl;
- if( n.getKind()==FORALL && !TermDb::hasInstConstAttr(n) ){
- getQuantifiersEngine()->registerQuantifier( n );
+ if( n.getKind()==FORALL ){
+ if( !options::cbqi() || options::recurseCbqi() || !TermDb::hasInstConstAttr(n) ){
+ getQuantifiersEngine()->registerQuantifier( n );
+ Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() done " << n << endl;
+ }
}
}
bool removeInstantiationInternal( Node q, std::vector< Node >& terms );
/** set instantiation level attr */
static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level );
+public:
/** flush lemmas */
void flushLemmas();
-public:
/** get instantiation */
Node getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false );
/** get instantiation */
projects / cvc5.git / commitdiff