namespace CVC4 {
+
+SubsortSymmetryBreaker::SubsortSymmetryBreaker(QuantifiersEngine* qe, context::Context* c) :
+d_qe(qe), d_conflict(c,false) {
+ d_true = NodeManager::currentNM()->mkConst( true );
+}
+
eq::EqualityEngine * SubsortSymmetryBreaker::getEqualityEngine() {
return ((uf::TheoryUF*)d_qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getEqualityEngine();
}
return ((uf::TheoryUF*)d_qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getStrongSolver();
}
-SubsortSymmetryBreaker::SubsortSymmetryBreaker(QuantifiersEngine* qe, context::Context* c) :
-d_qe(qe), d_conflict(c,false), d_max_dom_const_sort(c,0), d_has_dom_const_sort(c,false),
-d_fact_index(c,0), d_fact_list(c) {
- d_true = NodeManager::currentNM()->mkConst( true );
+SubsortSymmetryBreaker::TypeInfo::TypeInfo( context::Context * c ) :
+d_max_dom_const_sort(c,0), d_has_dom_const_sort(c,false) {
}
-SubsortSymmetryBreaker::TypeInfo::TypeInfo( SubsortSymmetryBreaker * ssb, context::Context * c ) :
-d_ssb( ssb ), d_dom_constants( c ), d_first_active( c, 0 ){
+SubsortSymmetryBreaker::SubSortInfo::SubSortInfo( context::Context * c ) :
+d_dom_constants( c ), d_first_active( c, 0 ){
d_dc_nodes = 0;
}
-unsigned SubsortSymmetryBreaker::TypeInfo::getNumDomainConstants() {
+unsigned SubsortSymmetryBreaker::SubSortInfo::getNumDomainConstants() {
if( d_nodes.empty() ){
return 0;
}else{
}
}
-Node SubsortSymmetryBreaker::TypeInfo::getDomainConstant( int i ) {
+Node SubsortSymmetryBreaker::SubSortInfo::getDomainConstant( int i ) {
if( i==0 ){
return d_nodes[0];
}else{
}
}
-Node SubsortSymmetryBreaker::TypeInfo::getFirstActive() {
+Node SubsortSymmetryBreaker::SubSortInfo::getFirstActive(eq::EqualityEngine * ee) {
if( d_first_active.get()<(int)d_nodes.size() ){
Node fa = d_nodes[d_first_active.get()];
- return d_ssb->getEqualityEngine()->hasTerm( fa ) ? fa : Node::null();
+ return ee->hasTerm( fa ) ? fa : Node::null();
}else{
return Node::null();
}
}
-SubsortSymmetryBreaker::TypeInfo * SubsortSymmetryBreaker::getTypeInfo( TypeNode tn, int sid ) {
+SubsortSymmetryBreaker::TypeInfo * SubsortSymmetryBreaker::getTypeInfo( TypeNode tn ) {
+ if( d_t_info.find( tn )==d_t_info.end() ){
+ d_t_info[tn] = new TypeInfo( d_qe->getSatContext() );
+ }
+ return d_t_info[tn];
+}
+
+SubsortSymmetryBreaker::SubSortInfo * SubsortSymmetryBreaker::getSubSortInfo( TypeNode tn, int sid ) {
if( d_type_info.find( sid )==d_type_info.end() ){
- d_type_info[sid] = new TypeInfo( this, d_qe->getSatContext() );
+ d_type_info[sid] = new SubSortInfo( d_qe->getSatContext() );
d_sub_sorts[tn].push_back( sid );
d_sid_to_type[sid] = tn;
}
if( si->isWellSorted( n ) ){
int sid = si->getSortId( n );
Trace("sym-break-debug") << "SSB: New eq class " << n << " : " << n.getType() << " : " << sid << std::endl;
- TypeInfo * ti = getTypeInfo( tn, sid );
+ SubSortInfo * ti = getSubSortInfo( tn, sid );
if( std::find( ti->d_nodes.begin(), ti->d_nodes.end(), n )==ti->d_nodes.end() ){
if( ti->d_nodes.empty() ){
//for first subsort, we add unit equality
ti->d_node_to_id[n] = ti->d_nodes.size();
ti->d_nodes.push_back( n );
}
- if( !d_has_dom_const_sort.get() ){
- d_has_dom_const_sort.set( true );
- d_max_dom_const_sort.set( sid );
+ TypeInfo * tti = getTypeInfo( tn );
+ if( !tti->d_has_dom_const_sort.get() ){
+ tti->d_has_dom_const_sort.set( true );
+ tti->d_max_dom_const_sort.set( sid );
}
}
}
void SubsortSymmetryBreaker::merge( Node a, Node b ) {
-
+ if( Trace.isOn("sym-break-debug") ){
+ SortInference * si = d_qe->getTheoryEngine()->getSortInference();
+ int as = si->getSortId( a );
+ int bs = si->getSortId( b );
+ Trace("sym-break-debug") << "SSB: New merge " << a.getType() << " :: " << a << " : " << as;
+ Trace("sym-break-debug") << " == " << b << " : " << bs << std::endl;
+ }
}
void SubsortSymmetryBreaker::assertDisequal( Node a, Node b ) {
-
+ if( Trace.isOn("sym-break-debug") ){
+ SortInference * si = d_qe->getTheoryEngine()->getSortInference();
+ int as = si->getSortId( a );
+ int bs = si->getSortId( b );
+ Trace("sym-break-debug") << "SSB: New assert disequal " << a.getType() << " :: " << a << " : " << as;
+ Trace("sym-break-debug") << " != " << b << " : " << bs << std::endl;
+ }
}
void SubsortSymmetryBreaker::processFirstActive( TypeNode tn, int sid, int curr_card ){
- TypeInfo * ti = getTypeInfo( tn, sid );
+ SubSortInfo * ti = getSubSortInfo( tn, sid );
if( (int)ti->getNumDomainConstants()<curr_card ){
+ //static int checkCount = 0;
+ //checkCount++;
+ //if( checkCount%1000==0 ){
+ // std::cout << "Check count = " << checkCount << std::endl;
+ //}
+
Trace("sym-break-dc-debug") << "Check for domain constants " << tn << " : " << sid << ", curr_card = " << curr_card << ", ";
Trace("sym-break-dc-debug") << "#domain constants = " << ti->getNumDomainConstants() << std::endl;
- Node fa = ti->getFirstActive();
+ Node fa = ti->getFirstActive(getEqualityEngine());
bool invalid = true;
while( invalid && !fa.isNull() && (int)ti->getNumDomainConstants()<curr_card ){
invalid = false;
}
ti->d_dc_nodes++;
Trace("sym-break-dc-debug") << "Get max type info..." << std::endl;
- Assert( d_has_dom_const_sort.get() );
- int msid = d_max_dom_const_sort.get();
- TypeInfo * max_ti = getTypeInfo( d_sid_to_type[msid], msid );
+ TypeInfo * tti = getTypeInfo( tn );
+ Assert( tti->d_has_dom_const_sort.get() );
+ int msid = tti->d_max_dom_const_sort.get();
+ SubSortInfo * max_ti = getSubSortInfo( d_sid_to_type[msid], msid );
Trace("sym-break-dc-debug") << "Swap nodes..." << std::endl;
//now, check if we can apply symmetry breaking to another sort
if( ti->getNumDomainConstants()>max_ti->getNumDomainConstants() ){
Trace("sym-break-dc") << "Max domain constant subsort for " << tn << " becomes " << sid << std::endl;
- d_max_dom_const_sort.set( sid );
+ tti->d_max_dom_const_sort.set( sid );
}else if( ti!=max_ti ){
//construct symmetry breaking lemma
//current domain constant must be disequal from all current ones
for( unsigned r=0; r<2; r++ ){
Node n = ((r==0)==(msid>sid)) ? fa : m;
Node on = ((r==0)==(msid>sid)) ? m : fa;
- TypeInfo * t = ((r==0)==(msid>sid)) ? max_ti : ti;
+ SubSortInfo * t = ((r==0)==(msid>sid)) ? max_ti : ti;
for( unsigned i=0; i<t->d_node_to_id[on]; i++ ){
cc.push_back( n.eqNode( t->d_nodes[i] ) );
}
lem = Rewriter::rewrite( lem );
if( std::find( d_lemmas.begin(), d_lemmas.end(), lem )==d_lemmas.end() ){
d_lemmas.push_back( lem );
- Trace("sym-break-lemma") << "*** Symmetry break lemma for " << tn << " (" << sid << "==" << d_max_dom_const_sort.get() << ") : ";
+ Trace("sym-break-lemma") << "*** Symmetry break lemma for " << tn << " (" << sid << "==" << tti->d_max_dom_const_sort.get() << ") : ";
Trace("sym-break-lemma") << lem << std::endl;
d_pending_lemmas.push_back( lem );
}
}
if( invalid ){
ti->d_first_active.set( ti->d_first_active + 1 );
- fa = ti->getFirstActive();
+ fa = ti->getFirstActive(getEqualityEngine());
}
}
}
}
-void SubsortSymmetryBreaker::printDebugTypeInfo( const char * c, TypeNode tn, int sid ) {
- Trace(c) << "TypeInfo( " << tn << ", " << sid << " ) = " << std::endl;
+void SubsortSymmetryBreaker::printDebugSubSortInfo( const char * c, TypeNode tn, int sid ) {
+ Trace(c) << "SubSortInfo( " << tn << ", " << sid << " ) = " << std::endl;
Trace(c) << " Domain constants : ";
- TypeInfo * ti = getTypeInfo( tn, sid );
+ SubSortInfo * ti = getSubSortInfo( tn, sid );
for( NodeList::const_iterator it = ti->d_dom_constants.begin(); it != ti->d_dom_constants.end(); ++it ){
Node dc = *it;
Trace(c) << dc << " ";
}
Trace(c) << std::endl;
- Trace(c) << " First active node : " << ti->getFirstActive() << std::endl;
-}
-
-
-void SubsortSymmetryBreaker::queueFact( Node n ) {
- d_fact_list.push_back( n );
- /*
- if( n.getKind()==EQUAL ){
- merge( n[0], n[1] );
- }else if( n.getKind()==NOT && n[0].getKind()==EQUAL ){
- assertDisequal( n[0][0], n[0][1] );
- }else{
- newEqClass( n );
- }
- */
+ Trace(c) << " First active node : " << ti->getFirstActive(getEqualityEngine()) << std::endl;
}
bool SubsortSymmetryBreaker::check( Theory::Effort level ) {
- d_pending_lemmas.clear();
Trace("sym-break-debug") << "SymBreak : check " << level << std::endl;
+ /*
while( d_fact_index.get()<d_fact_list.size() ){
Node f = d_fact_list[d_fact_index.get()];
d_fact_index.set( d_fact_index.get() + 1 );
newEqClass( f );
}
}
+ */
Trace("sym-break-debug") << "SymBreak : update first actives" << std::endl;
for( std::map< TypeNode, std::vector< int > >::iterator it = d_sub_sorts.begin(); it != d_sub_sorts.end(); ++it ){
int card = getStrongSolver()->getCardinality( it->first );
private:
class TypeInfo {
- private:
- SubsortSymmetryBreaker * d_ssb;
- //bool isActive( Node n, unsigned & deq );
public:
- TypeInfo( SubsortSymmetryBreaker * ssb, context::Context* c );
+ TypeInfo( context::Context* c );
+ context::CDO< int > d_max_dom_const_sort;
+ context::CDO< bool > d_has_dom_const_sort;
+ };
+ class SubSortInfo {
+ public:
+ SubSortInfo( context::Context* c );
//list of all nodes from this (sub)type
std::vector< Node > d_nodes;
//the current domain constants for this (sub)type
bool hasDomainConstant( Node n );
unsigned getNumDomainConstants();
Node getDomainConstant( int i );
- Node getFirstActive();
+ Node getFirstActive(eq::EqualityEngine * ee);
};
std::map< TypeNode, std::vector< int > > d_sub_sorts;
std::map< int, TypeNode > d_sid_to_type;
- std::map< int, TypeInfo * > d_type_info;
-
- //maximum domain constants sort
- context::CDO< int > d_max_dom_const_sort;
- context::CDO< bool > d_has_dom_const_sort;
+ std::map< TypeNode, TypeInfo * > d_t_info;
+ std::map< int, SubSortInfo * > d_type_info;
- TypeInfo * getTypeInfo( TypeNode tn, int sid );
+ TypeInfo * getTypeInfo( TypeNode tn );
+ SubSortInfo * getSubSortInfo( TypeNode tn, int sid );
void processFirstActive( TypeNode tn, int sid, int curr_card );
private:
//void printDebugNodeInfo( const char * c, Node n );
- void printDebugTypeInfo( const char * c, TypeNode tn, int sid );
+ void printDebugSubSortInfo( const char * c, TypeNode tn, int sid );
+ /** fact list */
+ std::vector< Node > d_pending_lemmas;
+ std::vector< Node > d_lemmas;
+public:
/** new node */
void newEqClass( Node n );
/** merge */
void merge( Node a, Node b );
/** assert disequal */
void assertDisequal( Node a, Node b );
- /** fact list */
- context::CDO< unsigned > d_fact_index;
- NodeList d_fact_list;
- std::vector< Node > d_pending_lemmas;
- std::vector< Node > d_lemmas;
-public:
- /** queue fact */
- void queueFact( Node n );
/** check */
bool check( Theory::Effort level );
};
d_cf->d_thss->getDisequalityPropagator()->assertDisequal(a, n, Node::null());
}
if( options::ufssSymBreak() ){
- //d_cf->d_thss->getSymmetryBreaker()->assertDisequal( a, n );
- d_cf->d_thss->getSymmetryBreaker()->queueFact( a.eqNode( n ).negate() );
+ d_cf->d_thss->getSymmetryBreaker()->assertDisequal( a, n );
}
}
setDisequal( b, n, t, false );
d_thss->getDisequalityPropagator()->merge(a, b);
}
if( options::ufssSymBreak() ){
- //d_thss->getSymmetryBreaker()->merge(a, b);
- d_thss->getSymmetryBreaker()->queueFact( a.eqNode( b ) );
+ d_thss->getSymmetryBreaker()->merge(a, b);
}
}
}
d_thss->getDisequalityPropagator()->assertDisequal(a, b, Node::null());
}
if( options::ufssSymBreak() ){
- //d_thss->getSymmetryBreaker()->assertDisequal(a, b);
- d_thss->getSymmetryBreaker()->queueFact( a.eqNode( b ).negate() );
+ d_thss->getSymmetryBreaker()->assertDisequal(a, b);
}
}
}
Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << n << " : " << n.getType() << std::endl;
c->newEqClass( n );
if( options::ufssSymBreak() ){
- //d_sym_break->newEqClass( n );
- d_sym_break->queueFact( n );
+ d_sym_break->newEqClass( n );
}
}
}
#include <vector>
#include "util/sort_inference.h"
+#include "theory/uf/options.h"
+//#include "theory/rewriter.h"
using namespace CVC4;
using namespace std;
namespace CVC4 {
-
void SortInference::UnionFind::print(const char * c){
for( std::map< int, int >::iterator it = d_eqc.begin(); it != d_eqc.end(); ++it ){
Trace(c) << "s_" << it->first << " = s_" << it->second << ", ";
}
+void SortInference::recordSubsort( int s ){
+ s = d_type_union_find.getRepresentative( s );
+ if( std::find( d_sub_sorts.begin(), d_sub_sorts.end(), s )==d_sub_sorts.end() ){
+ d_sub_sorts.push_back( s );
+ }
+}
+
void SortInference::printSort( const char* c, int t ){
int rt = d_type_union_find.getRepresentative( t );
if( d_type_types.find( rt )!=d_type_types.end() ){
std::map< Node, Node > var_bound;
process( assertions[i], var_bound );
}
- //print debug
- if( Trace.isOn("sort-inference") ){
- for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){
- Trace("sort-inference") << it->first << " : ";
- if( !d_op_arg_types[ it->first ].empty() ){
- Trace("sort-inference") << "( ";
- for( size_t i=0; i<d_op_arg_types[ it->first ].size(); i++ ){
- printSort( "sort-inference", d_op_arg_types[ it->first ][i] );
- Trace("sort-inference") << " ";
- }
- Trace("sort-inference") << ") -> ";
+ for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){
+ Trace("sort-inference") << it->first << " : ";
+ if( !d_op_arg_types[ it->first ].empty() ){
+ Trace("sort-inference") << "( ";
+ for( size_t i=0; i<d_op_arg_types[ it->first ].size(); i++ ){
+ recordSubsort( d_op_arg_types[ it->first ][i] );
+ printSort( "sort-inference", d_op_arg_types[ it->first ][i] );
+ Trace("sort-inference") << " ";
}
- printSort( "sort-inference", it->second );
- Trace("sort-inference") << std::endl;
+ Trace("sort-inference") << ") -> ";
}
- for( std::map< Node, std::map< Node, int > >::iterator it = d_var_types.begin(); it != d_var_types.end(); ++it ){
- Trace("sort-inference") << "Quantified formula " << it->first << " : " << std::endl;
- for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
- printSort( "sort-inference", it2->second );
- Trace("sort-inference") << std::endl;
- }
+ recordSubsort( it->second );
+ printSort( "sort-inference", it->second );
+ Trace("sort-inference") << std::endl;
+ }
+ for( std::map< Node, std::map< Node, int > >::iterator it = d_var_types.begin(); it != d_var_types.end(); ++it ){
+ Trace("sort-inference") << "Quantified formula : " << it->first << " : " << std::endl;
+ for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+ printSort( "sort-inference", it2->second );
Trace("sort-inference") << std::endl;
}
+ Trace("sort-inference") << std::endl;
+ }
+
+ //determine monotonicity of sorts
+ for( unsigned i=0; i<assertions.size(); i++ ){
+ Trace("sort-inference-debug") << "Process monotonicity for " << assertions[i] << std::endl;
+ std::map< Node, Node > var_bound;
+ processMonotonic( assertions[i], true, true, var_bound );
+ }
+
+ Trace("sort-inference") << "We have " << d_sub_sorts.size() << " sub-sorts : " << std::endl;
+ for( unsigned i=0; i<d_sub_sorts.size(); i++ ){
+ printSort( "sort-inference", d_sub_sorts[i] );
+ if( d_type_types.find( d_sub_sorts[i] )!=d_type_types.end() ){
+ Trace("sort-inference") << " is interpreted." << std::endl;
+ }else if( d_non_monotonic_sorts.find( d_sub_sorts[i] )==d_non_monotonic_sorts.end() ){
+ Trace("sort-inference") << " is monotonic." << std::endl;
+ }else{
+ Trace("sort-inference") << " is not monotonic." << std::endl;
+ }
}
+
if( doRewrite ){
//simplify all assertions by introducing new symbols wherever necessary (NOTE: this is unsound for quantifiers)
for( unsigned i=0; i<assertions.size(); i++ ){
}
//add lemma enforcing introduced constants to be distinct?
}
+ }else if( !options::ufssSymBreak() ){
+ std::map< int, Node > constants;
+ //just add a bunch of unit lemmas
+ for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){
+ int rt = d_type_union_find.getRepresentative( it->second );
+ if( d_op_arg_types[ it->first ].empty() && constants.find( rt )==constants.end() ){
+ constants[ rt ] = it->first;
+ }
+ }
+ //add unit lemmas for each constant
+ Node first_const;
+ for( std::map< int, Node >::iterator it = constants.begin(); it != constants.end(); ++it ){
+ if( first_const.isNull() ){
+ first_const = it->second;
+ }else{
+ Node eq = first_const.eqNode( it->second );
+ //eq = Rewriter::rewrite( eq );
+ Trace("sort-inference-lemma") << "Sort inference lemma : " << eq << std::endl;
+ assertions.push_back( eq );
+ }
+ }
+
+
}
initialSortCount = sortCount;
}
//d_type_eq_class[sortCount].push_back( n );
}
retType = d_op_return_types[n];
- }else if( n.isConst() ){
- Trace("sort-inference-debug") << n << " is a constant." << std::endl;
+ //}else if( n.isConst() ){
+ // Trace("sort-inference-debug") << n << " is a constant." << std::endl;
//can be any type we want
- retType = sortCount;
- sortCount++;
+ // retType = sortCount;
+ // sortCount++;
}else{
Trace("sort-inference-debug") << n << " is a interpreted symbol." << std::endl;
//it is an interpretted term
return retType;
}
+void SortInference::processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound ) {
+ if( n.getKind()==kind::FORALL ){
+ for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
+ var_bound[n[0][i]] = n;
+ }
+ processMonotonic( n[1], pol, hasPol, var_bound );
+ for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
+ var_bound.erase( n[0][i] );
+ }
+ }else if( n.getKind()==kind::EQUAL ){
+ if( !hasPol || pol ){
+ for( unsigned i=0; i<2; i++ ){
+ if( var_bound.find( n[i] )==var_bound.end() ){
+ int sid = getSortId( var_bound[n[i]], n[i] );
+ d_non_monotonic_sorts[sid] = true;
+ break;
+ }
+ }
+ }
+ }else{
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ bool npol = pol;
+ bool nhasPol = hasPol;
+ if( n.getKind()==kind::NOT || ( n.getKind()==kind::IMPLIES && i==0 ) ){
+ npol = !npol;
+ }
+ if( ( n.getKind()==kind::ITE && i==0 ) || n.getKind()==kind::XOR || n.getKind()==kind::IFF ){
+ nhasPol = false;
+ }
+ processMonotonic( n[i], npol, nhasPol, var_bound );
+ }
+ }
+}
+
TypeNode SortInference::getOrCreateTypeForId( int t, TypeNode pref ){
int rt = d_type_union_find.getRepresentative( t );
class SortInference{
private:
- //for debugging
- //std::map< int, std::vector< Node > > d_type_eq_class;
+ //all subsorts
+ std::vector< int > d_sub_sorts;
+ std::map< int, bool > d_non_monotonic_sorts;
+ void recordSubsort( int s );
public:
class UnionFind {
public:
void printSort( const char* c, int t );
//process
int process( Node n, std::map< Node, Node >& var_bound );
+
+//for monotonicity inference
+private:
+ void processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound );
+
+//for rewriting
private:
//mapping from old symbols to new symbols
std::map< Node, Node > d_symbol_map;
Node getNewSymbol( Node old, TypeNode tn );
//simplify
Node simplify( Node n, std::map< Node, Node >& var_bound );
+
public:
SortInference() : sortCount( 1 ){}
~SortInference(){}
projects / cvc5.git / commitdiff