summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/quantifiers/ce_guided_instantiation.cpp10
-rw-r--r--src/theory/quantifiers/ce_guided_single_inv.cpp112
-rw-r--r--src/theory/quantifiers/ce_guided_single_inv.h6
-rw-r--r--src/theory/quantifiers/term_database.cpp30
-rw-r--r--src/theory/quantifiers/term_database.h4
5 files changed, 144 insertions, 18 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 2044d612c..3475e9e97 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -477,7 +477,7 @@ void CegInstantiation::getMeasureLemmas( Node n, Node v, std::vector< Node >& le
void CegInstantiation::printSynthSolution( std::ostream& out ) {
if( d_conj ){
- if( !Trace.isOn("cegqi-stats") ){
+ if( !(Trace.isOn("cegqi-stats")) ){
out << "Solution:" << std::endl;
}
for( unsigned i=0; i<d_conj->d_candidates.size(); i++ ){
@@ -491,19 +491,21 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
Assert( dt.isSygus() );
//get the solution
Node sol;
+ int status;
if( d_last_inst_si ){
Assert( d_conj->d_ceg_si );
- sol = d_conj->d_ceg_si->getSolution( d_quantEngine, tn, i, Node::fromExpr( dt.getSygusVarList() ) );
+ sol = d_conj->d_ceg_si->getSolution( d_quantEngine, i, tn, status );
}else{
if( !d_conj->d_candidate_inst[i].empty() ){
sol = d_conj->d_candidate_inst[i].back();
+ status = 1;
}
}
- if( !Trace.isOn("cegqi-stats") ){
+ if( !(Trace.isOn("cegqi-stats")) ){
out << "(define-fun " << f << " ";
out << dt.getSygusVarList() << " ";
out << dt.getSygusType() << " ";
- if( d_last_inst_si ){
+ if( status==0 ){
out << sol;
}else{
if( sol.isNull() ){
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index be20dd7c0..e22674414 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -679,9 +679,11 @@ Node CegConjectureSingleInv::constructSolution( unsigned i, unsigned index ) {
}
}
-Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, TypeNode stn, unsigned i, Node varList ){
+Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, unsigned i, TypeNode stn, int& reconstructed ){
Assert( !d_lemmas_produced.empty() );
Node s = constructSolution( i, 0 );
+ const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
+ Node varList = Node::fromExpr( dt.getSygusVarList() );
//TODO : not in grammar
Node prog = d_quant[0][i];
Node prog_app = d_single_inv_app_map[prog];
@@ -697,6 +699,7 @@ Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, TypeNode stn,
d_orig_solution = s;
Trace("cegqi-si-debug-sol") << "Solution (pre-rewrite): " << d_orig_solution << std::endl;
s = pullITEs( s );
+ //s = flattenITEs( s );
//do standard rewriting
s = Rewriter::rewrite( s );
@@ -709,7 +712,7 @@ Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, TypeNode stn,
s = Rewriter::rewrite( s );
Trace("cegqi-si-debug-sol") << "Solution (post-rewrite): " << s << std::endl;
d_solution = s;
- if( options::cegqiSingleInvReconstruct() ){
+ if( options::cegqiSingleInvReconstruct() && !stn.isNull() ){
collectReconstructNodes( qe->getTermDatabaseSygus(), d_solution, stn, Node::null(), TypeNode::null(), false );
std::vector< TypeNode > rcons_tn;
for( std::map< TypeNode, std::map< Node, bool > >::iterator it = d_rcons_to_process.begin(); it != d_rcons_to_process.end(); ++it ){
@@ -723,7 +726,6 @@ Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, TypeNode stn,
Assert( !it->second.empty() );
rcons_tn.push_back( it->first );
}
- /*
bool success;
unsigned index = 0;
do {
@@ -733,17 +735,32 @@ Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, TypeNode stn,
if( it->second.empty() ){
to_erase.push_back( it->first );
}else{
- Node n = qe->getTermDatabase()->getEnumerateType( it->first, index );
-
+ Node ns = qe->getTermDatabase()->getEnumerateTerm( it->first, index );
+ Node nb = qe->getTermDatabaseSygus()->sygusToBuiltin( ns, it->first );
+ Node nr = Rewriter::rewrite( nb );//qe->getTermDatabaseSygus()->getNormalized( it->first, nb, false, false );
+ if( it->second.find( nr )!=it->second.end() ){
+ Trace("cegqi-si-rcons") << "...reconstructed " << ns << " for term " << nr << std::endl;
+ d_reconstructed[nr][it->first] = ns;
+ d_reconstructed_op[nr][it->first] = false;
+ setReconstructed( nr, it->first );
+ }
success = false;
}
}
for( unsigned i=0; i<to_erase.size(); i++ ){
+ Trace("cegqi-si-rcons") << "......reconstructed all terms for type " << to_erase[i] << std::endl;
d_rcons_to_process.erase( to_erase[i] );
}
index++;
+ if( index%100==0 ){
+ Trace("cegqi-si-rcons-debug") << "Tried " << index << " for each type." << std::endl;
+ }
+ if( success ){
+ reconstructed = 1;
+ }
}while( !success );
- */
+ }else{
+ reconstructed = 0;
}
if( Trace.isOn("cegqi-si-debug-sol") ){
//debug solution
@@ -900,6 +917,60 @@ bool CegConjectureSingleInv::pullITECondition( Node root, Node n_ite, std::vecto
}
}
+Node CegConjectureSingleInv::flattenITEs( Node n, bool rec ) {
+ if( n.getKind()==ITE ){
+ Trace("csi-simp-debug") << "Flatten ITE : " << n << std::endl;
+ Node ret;
+ Node n0 = rec ? flattenITEs( n[0] ) : n[0];
+ Node n1 = rec ? flattenITEs( n[1] ) : n[1];
+ Node n2 = rec ? flattenITEs( n[2] ) : n[2];
+ if( n0.getKind()==NOT ){
+ ret = NodeManager::currentNM()->mkNode( ITE, n0[0], n2, n1 );
+ }else if( n0.getKind()==AND || n0.getKind()==OR ){
+ std::vector< Node > children;
+ for( unsigned i=1; i<n0.getNumChildren(); i++ ){
+ children.push_back( n0[i] );
+ }
+ Node rem = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( n0.getKind(), children );
+ Node ret;
+ if( n0.getKind()==AND ){
+ ret = NodeManager::currentNM()->mkNode( ITE, rem, NodeManager::currentNM()->mkNode( n0[0], n1, n2 ), n2 );
+ }else{
+ ret = NodeManager::currentNM()->mkNode( ITE, rem, n1, NodeManager::currentNM()->mkNode( n0[0], n1, n2 ) );
+ }
+ }else{
+ if( n0.getKind()==ITE ){
+ n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ),
+ NodeManager::currentNM()->mkNode( AND, n0.negate(), n2 ) );
+ }else if( n0.getKind()==IFF ){
+ n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ),
+ NodeManager::currentNM()->mkNode( AND, n0.negate(), n1.negate() ) );
+ }else{
+ return NodeManager::currentNM()->mkNode( ITE, n0, n1, n2 );
+ }
+ ret = NodeManager::currentNM()->mkNode( ITE, n0, n1, n2 );
+ }
+ return flattenITEs( ret, false );
+ }else{
+ if( n.getNumChildren()>0 ){
+ std::vector< Node > children;
+ bool childChanged = false;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ Node nc = flattenITEs( n[i] );
+ children.push_back( nc );
+ childChanged = childChanged || nc!=n[i];
+ }
+ if( !childChanged ){
+ return n;
+ }else{
+ return NodeManager::currentNM()->mkNode( n.getKind(), children );
+ }
+ }else{
+ return n;
+ }
+ }
+}
+
// assign is from literals to booleans
// union_find is from args to values
@@ -1114,7 +1185,7 @@ Node CegConjectureSingleInv::simplifySolution( QuantifiersEngine * qe, Node sol,
void CegConjectureSingleInv::collectReconstructNodes( TermDbSygus * tds, Node t, TypeNode stn, Node parent, TypeNode pstn, bool ignoreBoolean ) {
if( ignoreBoolean && t.getType().isBoolean() ){
- if( t.getKind()==OR || t.getKind()==AND || t.getKind()==IFF || t.getKind()==ITE ){
+ if( t.getKind()==OR || t.getKind()==AND || t.getKind()==IFF || t.getKind()==ITE || t.getKind()==NOT ){ //FIXME
for( unsigned i=0; i<t.getNumChildren(); i++ ){
collectReconstructNodes( tds, t[i], stn, parent, pstn, ignoreBoolean );
}
@@ -1140,6 +1211,7 @@ void CegConjectureSingleInv::collectReconstructNodes( TermDbSygus * tds, Node t,
collectReconstructNodes( tds, t[i], stnc, t, stn, ignB );
}
d_reconstructed[t][stn] = Node::fromExpr( dt[arg].getSygusOp() );
+ d_reconstructed_op[t][stn] = true;
processed = true;
}else{
Trace("cegqi-si-rcons-debug") << " Type has kind " << t.getKind() << ", but argument mismatch, with parent " << parent << std::endl;
@@ -1150,6 +1222,7 @@ void CegConjectureSingleInv::collectReconstructNodes( TermDbSygus * tds, Node t,
Trace("cegqi-si-rcons") << "...Reconstruction needed for " << t << " sygus type " << dt.getName() << " with parent " << parent << std::endl;
}else{
d_reconstructed[t][stn] = Node::fromExpr( dt[carg].getSygusOp() );
+ d_reconstructed_op[t][stn] = false;
processed = true;
Trace("cegqi-si-rcons-debug") << " Type has constant." << std::endl;
}
@@ -1178,9 +1251,11 @@ void CegConjectureSingleInv::setReconstructed( Node t, TypeNode stn ) {
TypeNode stnc;
for( std::map< TypeNode, bool >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
stnc = it2->first;
- d_rcons_graph[ro][it->first][stnc][t].erase( it2->first );
+ d_rcons_graph[ro][it->first][stnc][t].erase( stn );
if( d_rcons_graph[ro][it->first][stnc][t].empty() ){
d_rcons_graph[ro][it->first][stnc].erase( t );
+ }else{
+ Trace("cegqi-si-rcons-debug") << " " << ( r==0 ? "child" : "parent" ) << " " << it->first << " now has " << d_rcons_graph[ro][it->first][stnc][t].size() << std::endl;
}
}
if( d_rcons_graph[ro][it->first][stnc].empty() ){
@@ -1198,6 +1273,27 @@ void CegConjectureSingleInv::setReconstructed( Node t, TypeNode stn ) {
}
}
+Node CegConjectureSingleInv::getReconstructedSolution( TypeNode stn, Node t ) {
+ std::map< TypeNode, Node >::iterator it = d_reconstructed[t].find( stn );
+ if( it!=d_reconstructed[t].end() ){
+ if( d_reconstructed_op[t][stn] ){
+ std::vector< Node > children;
+ children.push_back( it->second );
+ for( unsigned i=0; i<t.getNumChildren(); i++ ){
+ Node nc = getReconstructedSolution( stn, t[i] );
+ children.push_back( nc );
+ }
+ return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
+ }else{
+ return it->second;
+ }
+ }else{
+ Trace("cegqi-si-rcons-debug") << "*** error : missing reconstruction for " << t << std::endl;
+ Assert( false );
+ return Node::null();
+ }
+}
+
} \ No newline at end of file
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index afd7167f2..7667ccf11 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -76,7 +76,7 @@ public:
//check
void check( QuantifiersEngine * qe, std::vector< Node >& lems );
//get solution
- Node getSolution( QuantifiersEngine * qe, TypeNode stn, unsigned i, Node varList );
+ Node getSolution( QuantifiersEngine * qe, unsigned i, TypeNode stn, int& reconstructed );
//solution simplification
@@ -85,6 +85,7 @@ private:
void debugTermSize( Node sol, int& t_size, int& num_ite );
Node pullITEs( Node n );
bool pullITECondition( Node root, Node n, std::vector< Node >& conj, Node& t, Node& rem, int depth );
+ Node flattenITEs( Node n, bool rec = true );
Node simplifySolution( QuantifiersEngine * qe, Node sol, std::map< Node, bool >& assign,
std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& args, int status );
bool getAssign( QuantifiersEngine * qe, bool pol, Node n, std::map< Node, bool >& assign, std::vector< Node >& new_assign,
@@ -94,12 +95,15 @@ private:
private:
std::map< Node, std::vector< TypeNode > > d_rcons_processed;
std::map< Node, std::map< TypeNode, Node > > d_reconstructed;
+ std::map< Node, std::map< TypeNode, bool > > d_reconstructed_op;
std::map< Node, std::map< TypeNode, std::map< Node, std::map< TypeNode, bool > > > > d_rcons_graph[2];
std::map< TypeNode, std::map< Node, bool > > d_rcons_to_process;
// term t with sygus type st
void collectReconstructNodes( TermDbSygus * tds, Node t, TypeNode stn, Node parent, TypeNode pstn, bool ignoreBoolean );
// set reconstructed
void setReconstructed( Node t, TypeNode stn );
+ // get solution
+ Node getReconstructedSolution( TypeNode stn, Node t );
};
}
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 24d7cbb5c..c5a3cec4d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1400,6 +1400,26 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int
}
}
+Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) {
+ std::map< Node, Node >::iterator it = d_sygus_to_builtin[tn].find( n );
+ if( it==d_sygus_to_builtin[tn].end() ){
+ Assert( n.getKind()==APPLY_CONSTRUCTOR );
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ unsigned i = Datatype::indexOf( n.getOperator().toExpr() );
+ Assert( n.getNumChildren()==dt[i].getNumArgs() );
+ std::map< TypeNode, int > var_count;
+ std::map< int, Node > pre;
+ for( unsigned j=0; j<n.getNumChildren(); j++ ){
+ pre[j] = sygusToBuiltin( n[j], getArgType( dt[i], j ) );
+ }
+ Node ret = mkGeneric( dt, i, var_count, pre );
+ d_sygus_to_builtin[tn][n] = ret;
+ return ret;
+ }else{
+ return it->second;
+ }
+}
+
Node TermDbSygus::getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs ) {
return n;
if( n.getKind()==SKOLEM ){
@@ -1436,7 +1456,7 @@ Node TermDbSygus::getSygusNormalized( Node n, std::map< TypeNode, int >& var_cou
}
}
-Node TermDbSygus::getNormalized( TypeNode t, Node prog, bool do_pre_norm ) {
+Node TermDbSygus::getNormalized( TypeNode t, Node prog, bool do_pre_norm, bool do_post_norm ) {
if( do_pre_norm ){
std::map< TypeNode, int > var_count;
std::map< Node, Node > subs;
@@ -1446,9 +1466,11 @@ Node TermDbSygus::getNormalized( TypeNode t, Node prog, bool do_pre_norm ) {
if( itn==d_normalized[t].end() ){
Node progr = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( prog.toExpr() ) );
progr = Rewriter::rewrite( progr );
- std::map< TypeNode, int > var_count;
- std::map< Node, Node > subs;
- progr = getSygusNormalized( progr, var_count, subs );
+ if( do_post_norm ){
+ std::map< TypeNode, int > var_count;
+ std::map< Node, Node > subs;
+ progr = getSygusNormalized( progr, var_count, subs );
+ }
Trace("sygus-sym-break2") << "...rewrites to " << progr << std::endl;
d_normalized[t][prog] = progr;
return progr;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index ce3a52d1c..0f730929c 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -388,6 +388,7 @@ private:
std::map< TypeNode, std::map< Node, std::map< int, int > > > d_type_value_offset_status;
//normalized map
std::map< TypeNode, std::map< Node, Node > > d_normalized;
+ std::map< TypeNode, std::map< Node, Node > > d_sygus_to_builtin;
public:
TermDbSygus(){}
bool isRegistered( TypeNode tn );
@@ -425,8 +426,9 @@ public:
Node getTypeMaxValue( TypeNode tn );
TypeNode getSygusType( Node v );
Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre );
+ Node sygusToBuiltin( Node n, TypeNode tn );
Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs );
- Node getNormalized( TypeNode t, Node prog, bool do_pre_norm = false );
+ Node getNormalized( TypeNode t, Node prog, bool do_pre_norm = false, bool do_post_norm = true );
int getTermSize( Node n );
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback