diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-11 19:07:49 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-11 19:07:49 +0100 |
commit | 6893a60697e86eebccda6cc8e2e92cea7ee654e3 (patch) | |
tree | fc3be0417495e6c2e880fbab13cb7b044e303a54 /src/theory/quantifiers | |
parent | 2f930be0eb2d0ea7b8f96448dc2e353927a79b5c (diff) |
Better support for solving multiple functions with cegqi-si. Minor cleanup.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 225 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.h | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv_sol.cpp | 191 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 2 |
4 files changed, 227 insertions, 196 deletions
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 30eac03fb..616c51f54 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -271,23 +271,6 @@ void CegConjectureSingleInv::initialize() { } } } - - /* - //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; - } - } - */ } } } @@ -358,32 +341,6 @@ bool CegConjectureSingleInv::getVariableEliminationTerm( bool pol, bool hasPol, 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 ) { @@ -521,72 +478,91 @@ void CegConjectureSingleInv::check( std::vector< Node >& lems ) { 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; @@ -599,6 +575,38 @@ void CegConjectureSingleInv::check( std::vector< Node >& lems ) { } } +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 ); @@ -622,35 +630,34 @@ Node CegConjectureSingleInv::applyProgVarSubstitution( Node n, std::map< Node, i } } -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; } } diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index 4a9ed76fe..a1f9d5a1f 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -43,9 +43,12 @@ private: bool getVariableEliminationTerm( bool pol, bool active, Node v, Node n, TNode& s, int& status ); Node constructSolution( unsigned i, unsigned index ); - int classifyTerm( Node n, std::map< Node, int >& subs_from_model ); + bool classifyTerm( Node n, std::map< Node, int >& subs_from_model, std::vector< int >& vars ); void collectProgVars( Node n, std::vector< Node >& vars ); Node applyProgVarSubstitution( Node n, std::map< Node, int >& subs_from_model, std::vector< Node >& subs ); + //equalities processed + std::map< Node, std::map< Node, std::map< int, bool > > > d_eq_processed; + bool solveEquality( Node lhs, Node rhs, int v, std::map< Node, int >& subs_from_model, std::vector< Node >& subs ); public: CegConjectureSingleInv( QuantifiersEngine * qe, Node q, CegConjecture * p ); // original conjecture diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp index 02c4c3a28..7cefb0aec 100644 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp @@ -661,7 +661,7 @@ Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int // 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; @@ -756,100 +756,116 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in } } 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; } } } @@ -963,7 +979,10 @@ int CegConjectureSingleInvSol::allocate( Node n, TypeNode stn ) { 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; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index e3f73699b..08c8a7e3e 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1568,6 +1568,8 @@ Node TermDbSygus::builtinToSygusConst( Node c, TypeNode tn ) { sc = Node::fromExpr( dt[carg].getSygusOp() ); }else{ //TODO + + } d_builtin_const_to_sygus[tn][c] = sc; return sc; |