}
}
}
-
- /*
- //equality resolution
- for( unsigned j=0; j<conjuncts.size(); j++ ){
- Node conj = conjuncts[j];
- std::map< Node, std::vector< Node > > case_vals;
- bool exh = processSingleInvLiteral( conj, false, case_vals );
- Trace("cegqi-si-er") << "Conjunct " << conj << " gives equality restrictions, exh = " << exh << " : " << std::endl;
- for( std::map< Node, std::vector< Node > >::iterator it = case_vals.begin(); it != case_vals.end(); ++it ){
- Trace("cegqi-si-er") << " " << it->first << " -> ";
- for( unsigned k=0; k<it->second.size(); k++ ){
- Trace("cegqi-si-er") << it->second[k] << " ";
- }
- Trace("cegqi-si-er") << std::endl;
- }
- }
- */
}
}
}
return false;
}
-bool CegConjectureSingleInv::processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals ) {
- if( lit.getKind()==NOT ){
- return processSingleInvLiteral( lit[0], !pol, case_vals );
- }else if( ( lit.getKind()==OR && pol ) || ( lit.getKind()==AND && !pol ) ){
- bool exh = true;
- for( unsigned k=0; k<lit.getNumChildren(); k++ ){
- bool curr = processSingleInvLiteral( lit[k], pol, case_vals );
- exh = exh && curr;
- }
- return exh;
- }else if( lit.getKind()==IFF || lit.getKind()==EQUAL ){
- if( pol ){
- for( unsigned r=0; r<2; r++ ){
- std::map< Node, Node >::iterator it = d_single_inv_map_to_prog.find( lit[r] );
- if( it!=d_single_inv_map_to_prog.end() ){
- if( r==1 || d_single_inv_map_to_prog.find( lit[1] )==d_single_inv_map_to_prog.end() ){
- case_vals[it->second].push_back( lit[ r==0 ? 1 : 0 ] );
- return true;
- }
- }
- }
- }
- }
- return false;
-}
-
bool CegConjectureSingleInv::analyzeSygusConjunct( Node p, Node n, std::map< Node, std::vector< Node > >& children,
std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke,
std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) {
Trace("cegqi-engine-debug") << subs[index] << std::endl;
}
//try to improve substitutions : look for terms that contain terms in question
- if( !subs_from_model.empty() ){
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
- while( !eqcs_i.isFinished() ){
- Node r = *eqcs_i;
- int res = -1;
- Node slv_n;
- Node const_n;
- eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
- while( !eqc_i.isFinished() ){
- Node n = *eqc_i;
- if( slv_n.isNull() || const_n.isNull() ){
- std::vector< Node > vars;
- int curr_res = classifyTerm( n, subs_from_model );
- Trace("cegqi-si-debug2") << "Term : " << n << " classify : " << curr_res << std::endl;
- if( curr_res!=-2 ){
- if( curr_res!=-1 && slv_n.isNull() ){
- res = curr_res;
- slv_n = n;
- }else if( const_n.isNull() ){
- const_n = n;
- }
- //TODO : fairness
- if( !slv_n.isNull() && !const_n.isNull() ){
+ bool success;
+ do{
+ success = false;
+ if( !subs_from_model.empty() ){
+ std::map< int, std::vector< Node > > cls_terms;
+ std::map< Node, std::vector< int > > vars;
+ std::map< Node, std::map< int, std::vector< Node > > > node_eqc;
+ std::map< Node, Node > node_rep;
+ int vn_max = -1;
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
+ while( !eqcs_i.isFinished() ){
+ Node r = *eqcs_i;
+ TypeNode rtn = r.getType();
+ if( rtn.isInteger() || rtn.isReal() ){
+ eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+ while( !eqc_i.isFinished() ){
+ Node n = *eqc_i;
+ if( classifyTerm( n, subs_from_model, vars[n] ) ){
+ Trace("cegqi-si-debug") << "Term " << n << " in eqc " << r << " with " << vars[n].size() << " unset variables." << std::endl;
+ int vs = (int)vars[n].size();
+ cls_terms[vs].push_back( n );
+ node_eqc[r][vs].push_back( n );
+ node_rep[n] = r;
+ vn_max = vs>vn_max ? vs : vn_max;
}
+ ++eqc_i;
}
}
- ++eqc_i;
+ ++eqcs_i;
}
- if( !slv_n.isNull() && !const_n.isNull() ){
- if( slv_n.getType().isInteger() || slv_n.getType().isReal() ){
- Trace("cegqi-si-debug") << "Can possibly set " << d_single_inv_sk[res] << " based on " << slv_n << " = " << const_n << std::endl;
- subs_from_model.erase( d_single_inv_sk[res] );
- Node prev_subs_res = subs[res];
- subs[res] = d_single_inv_sk[res];
- Node eq = slv_n.eqNode( const_n );
- bool success = false;
- std::map< Node, Node > msum;
- if( QuantArith::getMonomialSumLit( eq, msum ) ){
- Trace("cegqi-si-debug") << "As monomial sum : " << std::endl;
- QuantArith::debugPrintMonomialSum( msum, "cegqi-si");
- Node veq;
- if( QuantArith::isolate( d_single_inv_sk[res], msum, veq, EQUAL ) ){
- Trace("cegqi-si-debug") << "Isolated for " << d_single_inv_sk[res] << " : " << veq << std::endl;
- Node sol;
- for( unsigned r=0; r<2; r++ ){
- if( veq[r]==d_single_inv_sk[res] ){
- sol = veq[ r==0 ? 1 : 0 ];
+ // will try processed, then unprocessed
+ for( unsigned p=0; p<2; p++ ){
+ Trace("cegqi-si-debug") << "Try " << ( p==0 ? "un" : "" ) << "processed equalities..." << std::endl;
+ //prefer smallest # variables first on LHS
+ for( int vn = 1; vn<=vn_max; vn++ ){
+ Trace("cegqi-si-debug") << " Having " << vn << " variables on LHS..." << std::endl;
+ for( unsigned i=0; i<cls_terms[vn].size(); i++ ){
+ Node lhs = cls_terms[vn][i];
+ Node r = node_rep[lhs];
+ //prefer smallest # variables on RHS
+ for( int vnc = 0; vnc<=vn_max; vnc++ ){
+ Trace("cegqi-si-debug") << " Having " << vnc << " variables on RHS..." << std::endl;
+ for( unsigned j=0; j<node_eqc[r][vnc].size(); j++ ){
+ Node rhs = node_eqc[r][vnc][j];
+ if( lhs!=rhs ){
+ Trace("cegqi-si-debug") << " try " << lhs << " " << rhs << std::endl;
+ //for each variable in LHS
+ for( unsigned k=0; k<vars[lhs].size(); k++ ){
+ int v = vars[lhs][k];
+ Trace("cegqi-si-debug") << " variable " << v << std::endl;
+ Assert( vars[lhs].size()==vn );
+ //check if already processed
+ bool proc = d_eq_processed[lhs][rhs].find( v )!=d_eq_processed[lhs][rhs].end();
+ if( proc==(p==1) ){
+ if( solveEquality( lhs, rhs, v, subs_from_model, subs ) ){
+ Trace("cegqi-si-debug") << "Success, set " << lhs << " " << rhs << " " << v << std::endl;
+ d_eq_processed[lhs][rhs][v] = true;
+ success = true;
+ break;
+ }
+ }
+ }
+ if( success ){ break; }
}
}
- if( !sol.isNull() ){
- sol = applyProgVarSubstitution( sol, subs_from_model, subs );
- Trace("cegqi-si-debug") << "Substituted solution is : " << sol << std::endl;
- subs[res] = sol;
- Trace("cegqi-engine") << " ...by arithmetic, " << d_single_inv_sk[res] << " -> " << sol << std::endl;
- success = true;
- }
+ if( success ){ break; }
}
+ if( success ){ break; }
}
- if( !success ){
- subs[res] = prev_subs_res;
- }
+ if( success ){ break; }
}
+ if( success ){ break; }
+ }
+ }
+ }while( !subs_from_model.empty() && success );
+
+ if( Trace.isOn("cegqi-si-warn") ){
+ if( !subs_from_model.empty() ){
+ Trace("cegqi-si-warn") << "Warning : could not find values for : " << std::endl;
+ for( std::map< Node, int >::iterator it = subs_from_model.begin(); it != subs_from_model.end(); ++it ){
+ Trace("cegqi-si-warn") << " " << it->first << std::endl;
}
- ++eqcs_i;
}
}
+
Node lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() );
lem = Rewriter::rewrite( lem );
Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl;
}
}
+bool CegConjectureSingleInv::solveEquality( Node lhs, Node rhs, int v, std::map< Node, int >& subs_from_model, std::vector< Node >& subs ) {
+ Trace("cegqi-si-debug") << "Can possibly set " << d_single_inv_sk[v] << " based on " << lhs << " = " << rhs << std::endl;
+ subs_from_model.erase( d_single_inv_sk[v] );
+ Node prev_subs_v = subs[v];
+ subs[v] = d_single_inv_sk[v];
+ Node eq = lhs.eqNode( rhs );
+ std::map< Node, Node > msum;
+ if( QuantArith::getMonomialSumLit( eq, msum ) ){
+ Trace("cegqi-si-debug") << "As monomial sum : " << std::endl;
+ QuantArith::debugPrintMonomialSum( msum, "cegqi-si");
+ Node veq;
+ if( QuantArith::isolate( d_single_inv_sk[v], msum, veq, EQUAL ) ){
+ Trace("cegqi-si-debug") << "Isolated for " << d_single_inv_sk[v] << " : " << veq << std::endl;
+ Node sol;
+ for( unsigned r=0; r<2; r++ ){
+ if( veq[r]==d_single_inv_sk[v] ){
+ sol = veq[ r==0 ? 1 : 0 ];
+ }
+ }
+ if( !sol.isNull() ){
+ sol = applyProgVarSubstitution( sol, subs_from_model, subs );
+ Trace("cegqi-si-debug") << "Substituted solution is : " << sol << std::endl;
+ subs[v] = sol;
+ Trace("cegqi-engine") << " ...by arithmetic, " << d_single_inv_sk[v] << " -> " << sol << std::endl;
+ return true;
+ }
+ }
+ }
+ subs[v] = prev_subs_v;
+ return false;
+}
+
Node CegConjectureSingleInv::applyProgVarSubstitution( Node n, std::map< Node, int >& subs_from_model, std::vector< Node >& subs ) {
std::vector< Node > vars;
collectProgVars( n, vars );
}
}
-int CegConjectureSingleInv::classifyTerm( Node n, std::map< Node, int >& subs_from_model ) {
+bool CegConjectureSingleInv::classifyTerm( Node n, std::map< Node, int >& subs_from_model, std::vector< int >& vars ) {
if( n.getKind()==SKOLEM ){
std::map< Node, int >::iterator it = subs_from_model.find( n );
if( it!=subs_from_model.end() ){
- return it->second;
+ if( std::find( vars.begin(), vars.end(), it->second )==vars.end() ){
+ vars.push_back( it->second );
+ }
+ return true;
}else{
// if it is symbolic argument, we are also fine
if( std::find( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), n )!=d_single_inv_arg_sk.end() ){
- return -1;
+ return true;
}else{
//if it is another program, we are also fine
if( std::find( d_single_inv_sk.begin(), d_single_inv_sk.end(), n )!=d_single_inv_sk.end() ){
- return -1;
+ return true;
}else{
- return -2;
+ return false;
}
}
}
}else{
- int curr_res = -1;
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- int res = classifyTerm( n[i], subs_from_model );
- if( res==-2 ){
- return res;
- }else if( res!=-1 ){
- curr_res = res;
+ if( !classifyTerm( n[i], subs_from_model, vars ) ){
+ return false;
}
}
- return curr_res;
+ return true;
}
}
// if it is not already reconstructed
if( d_reconstruct.find( itt->second )==d_reconstruct.end() ){
Trace("csi-rcons") << "...reconstructed " << ns << " for term " << nr << std::endl;
- bool do_check = getPathToRoot( itt->second );
+ bool do_check = true;//getPathToRoot( itt->second );
setReconstructed( itt->second, ns );
if( do_check ){
Trace("csi-rcons-debug") << "...path to root, try reconstruction." << std::endl;
}
}
if( status!=0 ){
- Trace("csi-rcons-debug") << "Try matching for " << id << "." << std::endl;
- //try other options
- //match against other constructors
- bool success;
- int c_index = 0;
- do{
- success = false;
- int index_found;
- std::vector< Node > args;
- if( d_qe->getTermDatabaseSygus()->getMatch( min_t, stn, index_found, args, karg, c_index ) ){
- success = true;
+ if( min_t.isConst() ){
+ Node min_t_c = d_qe->getTermDatabaseSygus()->builtinToSygusConst( min_t, stn );
+ if( !min_t_c.isNull() ){
+ d_reconstruct[id] = min_t_c;
status = 0;
- Node cons = Node::fromExpr( dt[index_found].getConstructor() );
- Trace("csi-rcons-debug") << "Try alternative for " << id << ", matching " << dt[index_found].getName() << " with children : " << std::endl;
- for( unsigned i=0; i<args.size(); i++ ){
- Trace("csi-rcons-debug") << " " << args[i] << std::endl;
- }
- if( !collectReconstructNodes( id, args, dt[index_found], d_reconstruct_op[id][cons], status ) ){
- d_reconstruct_op[id].erase( cons );
- status = 1;
- }else{
- c_index = index_found+1;
- }
}
- }while( success && status!=0 );
-
+ }
if( status!=0 ){
- // construct an equivalence class of terms that are equivalent to t
- if( d_rep[id]==id ){
- Trace("csi-rcons-debug") << "Try rewriting for " << id << "." << std::endl;
- //get equivalence class of term
- std::vector< Node > equiv;
- if( tn.isBoolean() ){
- Node curr = min_t;
- Node new_t;
- do{
- new_t = Node::null();
- if( curr.getKind()==EQUAL && ( curr[0].getType().isInteger() || curr[0].getType().isReal() ) ){
- new_t = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, curr[0], curr[1] ),
- NodeManager::currentNM()->mkNode( LEQ, curr[1], curr[0] ) );
- }else if( curr.getKind()==ITE ){
- new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ),
- NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[2] ) );
- }else if( curr.getKind()==IFF ){
- new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ),
- NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[1].negate() ) );
- }else if( curr.getKind()==OR || curr.getKind()==AND ){
- new_t = TermDb::simpleNegate( curr ).negate();
- }else if( curr.getKind()==NOT ){
- new_t = TermDb::simpleNegate( curr[0] );
- }else{
- new_t = NodeManager::currentNM()->mkNode( NOT, NodeManager::currentNM()->mkNode( NOT, curr ) );
- }
- if( !new_t.isNull() ){
- if( new_t!=min_t && std::find( equiv.begin(), equiv.end(), new_t )==equiv.end() ){
- curr = new_t;
- equiv.push_back( new_t );
+ Trace("csi-rcons-debug") << "Try matching for " << id << "." << std::endl;
+ //try other options
+ //match against other constructors
+ bool success;
+ int c_index = 0;
+ do{
+ success = false;
+ int index_found;
+ std::vector< Node > args;
+ if( d_qe->getTermDatabaseSygus()->getMatch( min_t, stn, index_found, args, karg, c_index ) ){
+ success = true;
+ status = 0;
+ Node cons = Node::fromExpr( dt[index_found].getConstructor() );
+ Trace("csi-rcons-debug") << "Try alternative for " << id << ", matching " << dt[index_found].getName() << " with children : " << std::endl;
+ for( unsigned i=0; i<args.size(); i++ ){
+ Trace("csi-rcons-debug") << " " << args[i] << std::endl;
+ }
+ if( !collectReconstructNodes( id, args, dt[index_found], d_reconstruct_op[id][cons], status ) ){
+ d_reconstruct_op[id].erase( cons );
+ status = 1;
+ }else{
+ c_index = index_found+1;
+ }
+ }
+ }while( success && status!=0 );
+
+ if( status!=0 ){
+ // construct an equivalence class of terms that are equivalent to t
+ if( d_rep[id]==id ){
+ Trace("csi-rcons-debug") << "Try rewriting for " << id << "." << std::endl;
+ //get equivalence class of term
+ std::vector< Node > equiv;
+ if( tn.isBoolean() ){
+ Node curr = min_t;
+ Node new_t;
+ do{
+ new_t = Node::null();
+ if( curr.getKind()==EQUAL && ( curr[0].getType().isInteger() || curr[0].getType().isReal() ) ){
+ new_t = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, curr[0], curr[1] ),
+ NodeManager::currentNM()->mkNode( LEQ, curr[1], curr[0] ) );
+ }else if( curr.getKind()==ITE ){
+ new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ),
+ NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[2] ) );
+ }else if( curr.getKind()==IFF ){
+ new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ),
+ NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[1].negate() ) );
+ }else if( curr.getKind()==OR || curr.getKind()==AND ){
+ new_t = TermDb::simpleNegate( curr ).negate();
+ }else if( curr.getKind()==NOT ){
+ new_t = TermDb::simpleNegate( curr[0] );
}else{
- new_t = Node::null();
+ new_t = NodeManager::currentNM()->mkNode( NOT, NodeManager::currentNM()->mkNode( NOT, curr ) );
}
+ if( !new_t.isNull() ){
+ if( new_t!=min_t && std::find( equiv.begin(), equiv.end(), new_t )==equiv.end() ){
+ curr = new_t;
+ equiv.push_back( new_t );
+ }else{
+ new_t = Node::null();
+ }
+ }
+ }while( !new_t.isNull() );
+ }
+ for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+ Kind k = d_qe->getTermDatabaseSygus()->getArgKind( stn, i );
+ if( k==AND || k==OR ){
+ equiv.push_back( NodeManager::currentNM()->mkNode( k, min_t, min_t ) );
+ equiv.push_back( NodeManager::currentNM()->mkNode( k, min_t, NodeManager::currentNM()->mkConst( k==AND ) ) );
}
- }while( !new_t.isNull() );
- }
- //assign ids to terms
- Trace("csi-rcons-debug") << "Term " << id << " is equivalent to " << equiv.size() << " terms : " << std::endl;
- std::vector< int > equiv_ids;
- for( unsigned i=0; i<equiv.size(); i++ ){
- Trace("csi-rcons-debug") << " " << equiv[i] << std::endl;
- if( d_rcons_to_id[stn].find( equiv[i] )==d_rcons_to_id[stn].end() ){
- int eq_id = allocate( equiv[i], stn );
- d_eqc.erase( eq_id );
- d_rep[eq_id] = id;
- d_eqc[id].push_back( eq_id );
- equiv_ids.push_back( eq_id );
- }else{
- equiv_ids.push_back( -1 );
}
- }
- // now, try each of them
- for( unsigned i=0; i<equiv.size(); i++ ){
- if( equiv_ids[i]!=-1 ){
- collectReconstructNodes( equiv[i], stn, status );
- //if one succeeds
- if( status==0 ){
- Node rsol = getReconstructedSolution( equiv_ids[i] );
- Assert( !rsol.isNull() );
- //set all members of the equivalence class that this is the reconstructed solution
- setReconstructed( id, rsol );
- break;
+ //assign ids to terms
+ Trace("csi-rcons-debug") << "Term " << id << " is equivalent to " << equiv.size() << " terms : " << std::endl;
+ std::vector< int > equiv_ids;
+ for( unsigned i=0; i<equiv.size(); i++ ){
+ Trace("csi-rcons-debug") << " " << equiv[i] << std::endl;
+ if( d_rcons_to_id[stn].find( equiv[i] )==d_rcons_to_id[stn].end() ){
+ int eq_id = allocate( equiv[i], stn );
+ d_eqc.erase( eq_id );
+ d_rep[eq_id] = id;
+ d_eqc[id].push_back( eq_id );
+ equiv_ids.push_back( eq_id );
+ }else{
+ equiv_ids.push_back( -1 );
}
}
+ // now, try each of them
+ for( unsigned i=0; i<equiv.size(); i++ ){
+ if( equiv_ids[i]!=-1 ){
+ collectReconstructNodes( equiv[i], stn, status );
+ //if one succeeds
+ if( status==0 ){
+ Node rsol = getReconstructedSolution( equiv_ids[i] );
+ Assert( !rsol.isNull() );
+ //set all members of the equivalence class that this is the reconstructed solution
+ setReconstructed( id, rsol );
+ break;
+ }
+ }
+ }
+ }else{
+ Trace("csi-rcons-debug") << "Do not try rewriting for " << id << ", rep = " << d_rep[id] << std::endl;
}
- }else{
- Trace("csi-rcons-debug") << "Do not try rewriting for " << id << ", rep = " << d_rep[id] << std::endl;
}
}
}
std::map< Node, int >::iterator it = d_rcons_to_id[stn].find( n );
if( it==d_rcons_to_id[stn].end() ){
int ret = d_id_count;
- Trace("csi-rcons-debug") << "id " << ret << " : " << n << std::endl;
+ if( Trace.isOn("csi-rcons-debug") ){
+ const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
+ Trace("csi-rcons-debug") << "id " << ret << " : " << n << " " << dt.getName() << std::endl;
+ }
d_id_node[d_id_count] = n;
d_id_type[d_id_count] = stn;
d_rep[d_id_count] = d_id_count;
projects / cvc5.git / commitdiff