theory/quantifiers/sygus_inference.h \
theory/quantifiers/sygus_sampler.cpp \
theory/quantifiers/sygus_sampler.h \
- theory/quantifiers/symmetry_breaking.cpp \
- theory/quantifiers/symmetry_breaking.h \
theory/quantifiers/term_database.cpp \
theory/quantifiers/term_database.h \
theory/quantifiers/term_enumeration.cpp \
read_only = true
help = "use cliques instead of splitting on demand to shrink model"
-[[option]]
- name = "ufssSymBreak"
- category = "regular"
- long = "uf-ss-sym-break"
- type = "bool"
- default = "false"
- read_only = true
- help = "finite model finding symmetry breaking techniques"
-
[[option]]
name = "ufssFairness"
category = "regular"
options::mbqiMode.set( quantifiers::MBQI_FMC );
}
}
- if( options::ufssSymBreak() ){
- options::sortInference.set( true );
- }
if( options::fmfFunWellDefinedRelevant() ){
if( !options::fmfFunWellDefined.wasSetByUser() ){
options::fmfFunWellDefined.set( true );
+++ /dev/null
-/********************* */
-/*! \file symmetry_breaking.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds, Paul Meng, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief symmetry breaking module
- **
- **/
-
-#include "theory/quantifiers/symmetry_breaking.h"
-
-#include <vector>
-
-#include "theory/quantifiers_engine.h"
-#include "theory/rewriter.h"
-#include "theory/sort_inference.h"
-#include "theory/theory_engine.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/uf/theory_uf_strong_solver.h"
-
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::theory;
-using namespace std;
-
-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();
-}
-
-bool SubsortSymmetryBreaker::areEqual( Node n1, Node n2 ) {
- return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areEqual( n1,n2 );
-}
-
-bool SubsortSymmetryBreaker::areDisequal( Node n1, Node n2 ) {
- return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false );
-}
-
-
-Node SubsortSymmetryBreaker::getRepresentative( Node n ) {
- return getEqualityEngine()->getRepresentative( n );
-}
-
-uf::StrongSolverTheoryUF * SubsortSymmetryBreaker::getStrongSolver() {
- return ((uf::TheoryUF*)d_qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getStrongSolver();
-}
-
-SubsortSymmetryBreaker::TypeInfo::TypeInfo( context::Context * c ) :
-d_max_dom_const_sort(c,0), d_has_dom_const_sort(c,false) {
-}
-
-SubsortSymmetryBreaker::SubSortInfo::SubSortInfo( context::Context * c ) :
-d_dom_constants( c ), d_first_active( c, 0 ){
- d_dc_nodes = 0;
-}
-
-unsigned SubsortSymmetryBreaker::SubSortInfo::getNumDomainConstants() {
- if( d_nodes.empty() ){
- return 0;
- }else{
- return 1 + d_dom_constants.size();
- }
-}
-
-Node SubsortSymmetryBreaker::SubSortInfo::getDomainConstant( int i ) {
- if( i==0 ){
- return d_nodes[0];
- }else{
- Assert( i<=(int)d_dom_constants.size() );
- return d_dom_constants[i-1];
- }
-}
-
-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 ee->hasTerm( fa ) ? fa : Node::null();
- }else{
- return Node::null();
- }
-}
-
-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 SubSortInfo( d_qe->getSatContext() );
- d_sub_sorts[tn].push_back( sid );
- d_sid_to_type[sid] = tn;
- }
- return d_type_info[sid];
-}
-
-void SubsortSymmetryBreaker::newEqClass( Node n ) {
- Trace("sym-break-temp") << "New eq class " << n << std::endl;
- if( !d_conflict ){
- TypeNode tn = n.getType();
- SortInference * si = d_qe->getTheoryEngine()->getSortInference();
- if( si->isWellSorted( n ) ){
- int sid = si->getSortId( n );
- Trace("sym-break-debug") << "SSB: New eq class " << n << " : " << n.getType() << " : " << sid << std::endl;
- 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
- if( d_sub_sorts[tn][0]!=sid ){
- Trace("sym-break-temp") << "Do sym break unit with " << d_type_info[d_sub_sorts[tn][0]]->getBaseConstant() << std::endl;
- //add unit symmetry breaking lemma
- Node eq = n.eqNode( d_type_info[d_sub_sorts[tn][0]]->getBaseConstant() );
- eq = Rewriter::rewrite( eq );
- d_unit_lemmas.push_back( eq );
- Trace("sym-break-lemma") << "*** SymBreak : Unit lemma (" << sid << "==" << d_sub_sorts[tn][0] << ") : " << eq << std::endl;
- d_pending_lemmas.push_back( eq );
- }
- Trace("sym-break-dc") << "* Set first domain constant : " << n << " for " << tn << " : " << sid << std::endl;
- ti->d_dc_nodes++;
- }
- ti->d_node_to_id[n] = ti->d_nodes.size();
- ti->d_nodes.push_back( n );
- }
- 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 );
- }
- }
- }
- Trace("sym-break-temp") << "Done new eq class" << std::endl;
-}
-
-
-
-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 ){
- 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(getEqualityEngine());
- bool invalid = true;
- while( invalid && !fa.isNull() && (int)ti->getNumDomainConstants()<curr_card ){
- invalid = false;
- unsigned deq = 0;
- for( unsigned i=0; i<ti->getNumDomainConstants(); i++ ){
- Node dc = ti->getDomainConstant( i );
- if( areEqual( fa, dc ) ){
- invalid = true;
- break;
- }else if( areDisequal( fa, dc ) ){
- deq++;
- }
- }
- if( deq==ti->getNumDomainConstants() ){
- Trace("sym-break-dc") << "* Can infer domain constant #" << ti->getNumDomainConstants()+1;
- Trace("sym-break-dc") << " : " << fa << " for " << tn << " : " << sid << std::endl;
- //add to domain constants
- ti->d_dom_constants.push_back( fa );
- if( ti->d_node_to_id[fa]>ti->d_dc_nodes ){
- Trace("sym-break-dc-debug") << "Swap nodes... " << ti->d_dc_nodes << " " << ti->d_node_to_id[fa] << " " << ti->d_nodes.size() << std::endl;
- //swap
- Node on = ti->d_nodes[ti->d_dc_nodes];
- int id = ti->d_node_to_id[fa];
-
- ti->d_nodes[ti->d_dc_nodes] = fa;
- ti->d_nodes[id] = on;
- ti->d_node_to_id[fa] = ti->d_dc_nodes;
- ti->d_node_to_id[on] = id;
- }
- ti->d_dc_nodes++;
- Trace("sym-break-dc-debug") << "Get max type info..." << std::endl;
- 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;
- 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
- Trace("sym-break-dc") << "Get domain constant " << ti->getNumDomainConstants()-1;
- Trace("sym-break-dc") << " from max_ti, " << max_ti->getNumDomainConstants() << std::endl;
- //apply a symmetry breaking lemma
- Node m = max_ti->getDomainConstant(ti->getNumDomainConstants()-1);
- //if fa and m are disequal from all previous domain constants in the other sort
- std::vector< Node > cc;
- for( unsigned r=0; r<2; r++ ){
- Node n = ((r==0)==(msid>sid)) ? fa : m;
- Node on = ((r==0)==(msid>sid)) ? m : fa;
- 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] ) );
- }
- }
- //then, we can assume fa = m
- cc.push_back( fa.eqNode( m ) );
- Node lem = NodeManager::currentNM()->mkNode( kind::OR, cc );
- 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 << "==" << tti->d_max_dom_const_sort.get() << ") : ";
- Trace("sym-break-lemma") << lem << std::endl;
- d_pending_lemmas.push_back( lem );
- }
- }
- invalid = true;
- }
- if( invalid ){
- ti->d_first_active.set( ti->d_first_active + 1 );
- fa = ti->getFirstActive(getEqualityEngine());
- }
- }
- }
-}
-
-void SubsortSymmetryBreaker::printDebugSubSortInfo( const char * c, TypeNode tn, int sid ) {
- Trace(c) << "SubSortInfo( " << tn << ", " << sid << " ) = " << std::endl;
- Trace(c) << " Domain constants : ";
- 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(getEqualityEngine()) << std::endl;
-}
-
-bool SubsortSymmetryBreaker::check( Theory::Effort level ) {
-
- 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 );
- if( f.getKind()==EQUAL ){
- merge( f[0], f[1] );
- }else if( f.getKind()==NOT && f[0].getKind()==EQUAL ){
- assertDisequal( f[0][0], f[0][1] );
- }else{
- 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 );
- for( unsigned i=0; i<it->second.size(); i++ ){
- //check if the first active is disequal from all domain constants
- processFirstActive( it->first, it->second[i], card );
- }
- }
-
-
- Trace("sym-break-debug") << "SymBreak : finished check, now flush lemmas... (#lemmas = " << d_pending_lemmas.size() << ")" << std::endl;
- //flush pending lemmas
- if( !d_pending_lemmas.empty() ){
- for( unsigned i=0; i<d_pending_lemmas.size(); i++ ){
- getStrongSolver()->getOutputChannel().lemma( d_pending_lemmas[i], false, true );
- ++( getStrongSolver()->d_statistics.d_sym_break_lemmas );
- }
- d_pending_lemmas.clear();
- return true;
- }else{
- return false;
- }
-}
-
-
-
-}
-
+++ /dev/null
-/********************* */
-/*! \file symmetry_breaking.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Pre-process step for first-order reasoning
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__QUANT_SYMMETRY_BREAKING_H
-#define __CVC4__QUANT_SYMMETRY_BREAKING_H
-
-#include <iostream>
-#include <map>
-#include <string>
-#include <vector>
-
-#include "context/cdhashmap.h"
-#include "context/context.h"
-#include "context/context_mm.h"
-#include "expr/node.h"
-#include "expr/type_node.h"
-#include "theory/sort_inference.h"
-#include "theory/theory.h"
-
-namespace CVC4 {
-namespace theory {
-
-namespace uf {
- class StrongSolverTheoryUF;
-}
-
-class SubsortSymmetryBreaker {
- typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
- typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
- typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
- typedef context::CDList<Node> NodeList;
-private:
- /** quantifiers engine */
- QuantifiersEngine* d_qe;
- eq::EqualityEngine * getEqualityEngine();
- bool areDisequal( Node n1, Node n2 );
- bool areEqual( Node n1, Node n2 );
- Node getRepresentative( Node n );
- uf::StrongSolverTheoryUF * getStrongSolver();
- std::vector< Node > d_unit_lemmas;
- Node d_true;
- context::CDO< bool > d_conflict;
-public:
- SubsortSymmetryBreaker( QuantifiersEngine* qe, context::Context* c );
- ~SubsortSymmetryBreaker(){}
-
-private:
- class TypeInfo {
- public:
- 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
- NodeList d_dom_constants;
- //# nodes in d_nodes that have been domain constants, size of this distinct # of domain constants seen
- unsigned d_dc_nodes;
- //the node we are currently watching to become a domain constant
- context::CDO< int > d_first_active;
- //node to id
- std::map< Node, unsigned > d_node_to_id;
- Node getBaseConstant() { return d_nodes.empty() ? Node::null() : d_nodes[0]; }
- bool hasDomainConstant( Node n );
- unsigned getNumDomainConstants();
- Node getDomainConstant( int i );
- Node getFirstActive(eq::EqualityEngine * ee);
- };
- std::map< TypeNode, std::vector< int > > d_sub_sorts;
- std::map< int, TypeNode > d_sid_to_type;
- std::map< TypeNode, TypeInfo * > d_t_info;
- std::map< int, SubSortInfo * > d_type_info;
-
- 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 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 );
- /** check */
- bool check( Theory::Effort level );
-};
-
-}
-}
-
-#endif
void SortInference::simplify( std::vector< Node >& assertions, bool doSortInference, bool doMonotonicyInference ){
if( doSortInference ){
Trace("sort-inference-proc") << "Calculating sort inference..." << std::endl;
+ NodeManager* nm = NodeManager::currentNM();
//process all assertions
std::map< Node, int > visited;
for( unsigned i=0; i<assertions.size(); i++ ){
Trace("sort-inference") << std::endl;
}
- if( !options::ufssSymBreak() ){
- bool rewritten = false;
- //determine monotonicity of sorts
- Trace("sort-inference-proc") << "Calculating monotonicty for subsorts..." << std::endl;
- std::map< Node, std::map< int, bool > > visited;
- 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, visited );
- }
- Trace("sort-inference-proc") << "...done" << std::endl;
-
- 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;
- }
+ bool rewritten = false;
+ // determine monotonicity of sorts
+ Trace("sort-inference-proc") << "Calculating monotonicty for subsorts..."
+ << std::endl;
+ std::map<Node, std::map<int, bool> > visitedm;
+ for (const Node& a : assertions)
+ {
+ Trace("sort-inference-debug") << "Process monotonicity for " << a
+ << std::endl;
+ std::map<Node, Node> var_bound;
+ processMonotonic(a, true, true, var_bound, visitedm);
+ }
+ Trace("sort-inference-proc") << "...done" << std::endl;
+
+ Trace("sort-inference") << "We have " << d_sub_sorts.size()
+ << " sub-sorts : " << std::endl;
+ for (unsigned i = 0, size = d_sub_sorts.size(); i < 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;
}
+ }
- //simplify all assertions by introducing new symbols wherever necessary
- Trace("sort-inference-proc") << "Perform simplification..." << std::endl;
- std::map< Node, std::map< TypeNode, Node > > visited2;
- for( unsigned i=0; i<assertions.size(); i++ ){
- Node prev = assertions[i];
- std::map< Node, Node > var_bound;
- Trace("sort-inference-debug") << "Simplify " << assertions[i] << std::endl;
- TypeNode tnn;
- Node curr = simplifyNode( assertions[i], var_bound, tnn, visited2 );
- Trace("sort-inference-debug") << "Done." << std::endl;
- if( curr!=assertions[i] ){
- Trace("sort-inference-debug") << "Rewrite " << curr << std::endl;
- curr = theory::Rewriter::rewrite( curr );
- rewritten = true;
- Trace("sort-inference-rewrite") << assertions << std::endl;
- Trace("sort-inference-rewrite") << " --> " << curr << std::endl;
- PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); );
- assertions[i] = curr;
- }
+ // simplify all assertions by introducing new symbols wherever necessary
+ Trace("sort-inference-proc") << "Perform simplification..." << std::endl;
+ std::map<Node, std::map<TypeNode, Node> > visited2;
+ for (unsigned i = 0, size = assertions.size(); i < size; i++)
+ {
+ Node prev = assertions[i];
+ std::map<Node, Node> var_bound;
+ Trace("sort-inference-debug") << "Simplify " << prev << std::endl;
+ TypeNode tnn;
+ Node curr = simplifyNode(assertions[i], var_bound, tnn, visited2);
+ Trace("sort-inference-debug") << "Done." << std::endl;
+ if (curr != assertions[i])
+ {
+ Trace("sort-inference-debug") << "Rewrite " << curr << std::endl;
+ curr = theory::Rewriter::rewrite(curr);
+ rewritten = true;
+ Trace("sort-inference-rewrite") << assertions << std::endl;
+ Trace("sort-inference-rewrite") << " --> " << curr << std::endl;
+ PROOF(ProofManager::currentPM()->addDependence(curr, assertions[i]););
+ assertions[i] = curr;
}
- Trace("sort-inference-proc") << "...done" << std::endl;
- //now, ensure constants are distinct
- for( std::map< TypeNode, std::map< Node, Node > >::iterator it = d_const_map.begin(); it != d_const_map.end(); ++it ){
- std::vector< Node > consts;
- for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
- Assert( it2->first.isConst() );
- consts.push_back( it2->second );
- }
- //add lemma enforcing introduced constants to be distinct
- if( consts.size()>1 ){
- Node distinct_const = NodeManager::currentNM()->mkNode( kind::DISTINCT, consts );
- Trace("sort-inference-rewrite") << "Add the constant distinctness lemma: " << std::endl;
- Trace("sort-inference-rewrite") << " " << distinct_const << std::endl;
- assertions.push_back( distinct_const );
- rewritten = true;
- }
+ }
+ Trace("sort-inference-proc") << "...done" << std::endl;
+ // now, ensure constants are distinct
+ for (std::map<TypeNode, std::map<Node, Node> >::iterator it =
+ d_const_map.begin();
+ it != d_const_map.end();
+ ++it)
+ {
+ std::vector<Node> consts;
+ for (std::map<Node, Node>::iterator it2 = it->second.begin();
+ it2 != it->second.end();
+ ++it2)
+ {
+ Assert(it2->first.isConst());
+ consts.push_back(it2->second);
+ }
+ // add lemma enforcing introduced constants to be distinct
+ if (consts.size() > 1)
+ {
+ Node distinct_const = nm->mkNode(kind::DISTINCT, consts);
+ Trace("sort-inference-rewrite")
+ << "Add the constant distinctness lemma: " << std::endl;
+ Trace("sort-inference-rewrite") << " " << distinct_const << std::endl;
+ assertions.push_back(distinct_const);
+ rewritten = true;
}
+ }
- //enforce constraints based on monotonicity
- Trace("sort-inference-proc") << "Enforce monotonicity..." << std::endl;
- for( std::map< TypeNode, std::vector< int > >::iterator it = d_type_sub_sorts.begin(); it != d_type_sub_sorts.end(); ++it ){
- int nmonSort = -1;
- for( unsigned i=0; i<it->second.size(); i++ ){
- if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){
- nmonSort = it->second[i];
- break;
- }
+ // enforce constraints based on monotonicity
+ Trace("sort-inference-proc") << "Enforce monotonicity..." << std::endl;
+ for (std::map<TypeNode, std::vector<int> >::iterator it =
+ d_type_sub_sorts.begin();
+ it != d_type_sub_sorts.end();
+ ++it)
+ {
+ int nmonSort = -1;
+ unsigned nsorts = it->second.size();
+ for (unsigned i = 0; i < nsorts; i++)
+ {
+ if (d_non_monotonic_sorts.find(it->second[i])
+ != d_non_monotonic_sorts.end())
+ {
+ nmonSort = it->second[i];
+ break;
}
- if( nmonSort!=-1 ){
- std::vector< Node > injections;
- TypeNode base_tn = getOrCreateTypeForId( nmonSort, it->first );
- for( unsigned i=0; i<it->second.size(); i++ ){
- if( it->second[i]!=nmonSort ){
- TypeNode new_tn = getOrCreateTypeForId( it->second[i], it->first );
- //make injection to nmonSort
- Node a1 = mkInjection( new_tn, base_tn );
- injections.push_back( a1 );
- if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){
- //also must make injection from nmonSort to this
- Node a2 = mkInjection( base_tn, new_tn );
- injections.push_back( a2 );
- }
+ }
+ if (nmonSort != -1)
+ {
+ std::vector<Node> injections;
+ TypeNode base_tn = getOrCreateTypeForId(nmonSort, it->first);
+ for (unsigned i = 0; i < nsorts; i++)
+ {
+ if (it->second[i] != nmonSort)
+ {
+ TypeNode new_tn = getOrCreateTypeForId(it->second[i], it->first);
+ // make injection to nmonSort
+ Node a1 = mkInjection(new_tn, base_tn);
+ injections.push_back(a1);
+ if (d_non_monotonic_sorts.find(it->second[i])
+ != d_non_monotonic_sorts.end())
+ {
+ // also must make injection from nmonSort to this
+ Node a2 = mkInjection(base_tn, new_tn);
+ injections.push_back(a2);
}
}
+ }
+ if (Trace.isOn("sort-inference-rewrite"))
+ {
Trace("sort-inference-rewrite") << "Add the following injections for " << it->first << " to ensure consistency wrt non-monotonic sorts : " << std::endl;
- for( unsigned j=0; j<injections.size(); j++ ){
- Trace("sort-inference-rewrite") << " " << injections[j] << std::endl;
- }
- assertions.insert( assertions.end(), injections.begin(), injections.end() );
- if( !injections.empty() ){
- rewritten = true;
+ for (const Node& i : injections)
+ {
+ Trace("sort-inference-rewrite") << " " << i << std::endl;
}
}
+ assertions.insert(
+ assertions.end(), injections.begin(), injections.end());
+ if (!injections.empty())
+ {
+ rewritten = true;
+ }
}
- Trace("sort-inference-proc") << "...done" << std::endl;
- //no sub-sort information is stored
- reset();
- Trace("sort-inference-debug") << "Finished sort inference, rewritten = " << rewritten << std::endl;
}
+ Trace("sort-inference-proc") << "...done" << std::endl;
+ // no sub-sort information is stored
+ reset();
+ Trace("sort-inference-debug")
+ << "Finished sort inference, rewritten = " << rewritten << std::endl;
+
initialSortCount = sortCount;
}
if( doMonotonicyInference ){
- std::map< Node, std::map< int, bool > > visited;
+ std::map<Node, std::map<int, bool> > visitedmt;
Trace("sort-inference-proc") << "Calculating monotonicty for types..." << std::endl;
- for( unsigned i=0; i<assertions.size(); i++ ){
- Trace("sort-inference-debug") << "Process type monotonicity for " << assertions[i] << std::endl;
+ for (const Node& a : assertions)
+ {
+ Trace("sort-inference-debug") << "Process type monotonicity for " << a
+ << std::endl;
std::map< Node, Node > var_bound;
- processMonotonic( assertions[i], true, true, var_bound, visited, true );
+ processMonotonic(a, true, true, var_bound, visitedmt, true);
}
Trace("sort-inference-proc") << "...done" << std::endl;
}
#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/term_database.h"
#include "theory/theory_model.h"
-#include "theory/quantifiers/symmetry_breaking.h"
//#define ONE_SPLIT_REGION
//#define DISABLE_QUICK_CLIQUE_CHECKS
if( !isDisequal( a, n, t ) ){
setDisequal( a, n, t, true );
nr->setDisequal( n, a, t, true );
- if( options::ufssSymBreak() ){
- d_cf->d_thss->getSymmetryBreaker()->assertDisequal( a, n );
- }
}
setDisequal( b, n, t, false );
nr->setDisequal( n, b, t, false );
d_regions_map[b] = -1;
}
d_reps = d_reps - 1;
-
- if( !d_conflict ){
- if( options::ufssSymBreak() ){
- d_thss->getSymmetryBreaker()->merge(a, b);
- }
- }
}
}
}
checkRegion( ai );
checkRegion( bi );
}
-
- if( !d_conflict ){
- if( options::ufssSymBreak() ){
- d_thss->getSymmetryBreaker()->assertDisequal(a, b);
- }
- }
}
}
}
StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c,
context::UserContext* u,
- OutputChannel& out, TheoryUF* th)
+ OutputChannel& out,
+ TheoryUF* th)
: d_out(&out),
d_th(th),
d_conflict(c, false),
d_min_pos_com_card(c, -1),
d_card_assertions_eqv_lemma(u),
d_min_pos_tn_master_card(c, -1),
- d_rel_eqc(c),
- d_sym_break(NULL) {
- if (options::ufssSymBreak()) {
- d_sym_break = new SubsortSymmetryBreaker(th->getQuantifiersEngine(), c);
- }
+ d_rel_eqc(c)
+{
}
StrongSolverTheoryUF::~StrongSolverTheoryUF() {
it != d_rep_model.end(); ++it) {
delete it->second;
}
- if (d_sym_break) {
- delete d_sym_break;
- }
}
SortInference* StrongSolverTheoryUF::getSortInference() {
d_rel_eqc[a] = true;
Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << a << " : " << a.getType() << std::endl;
c->newEqClass( a );
- if( options::ufssSymBreak() ){
- d_sym_break->newEqClass( a );
- }
Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl;
}
}
#else
Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << a << " : " << a.getType() << std::endl;
c->newEqClass( a );
- if( options::ufssSymBreak() ){
- d_sym_break->newEqClass( a );
- }
Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl;
#endif
}
break;
}
}
- //check symmetry breaker
- if( !d_conflict && options::ufssSymBreak() ){
- d_sym_break->check( level );
- }
}else if( options::ufssMode()==UF_SS_NO_MINIMAL ){
if( level==Theory::EFFORT_FULL ){
// split on an equality between two equivalence classes (at most one per type)
d_clique_lemmas("StrongSolverTheoryUF::Clique_Lemmas", 0),
d_split_lemmas("StrongSolverTheoryUF::Split_Lemmas", 0),
d_disamb_term_lemmas("StrongSolverTheoryUF::Disambiguate_Term_Lemmas", 0),
- d_sym_break_lemmas("StrongSolverTheoryUF::Symmetry_Breaking_Lemmas", 0),
d_totality_lemmas("StrongSolverTheoryUF::Totality_Lemmas", 0),
d_max_model_size("StrongSolverTheoryUF::Max_Model_Size", 1)
{
smtStatisticsRegistry()->registerStat(&d_clique_lemmas);
smtStatisticsRegistry()->registerStat(&d_split_lemmas);
smtStatisticsRegistry()->registerStat(&d_disamb_term_lemmas);
- smtStatisticsRegistry()->registerStat(&d_sym_break_lemmas);
smtStatisticsRegistry()->registerStat(&d_totality_lemmas);
smtStatisticsRegistry()->registerStat(&d_max_model_size);
}
smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas);
smtStatisticsRegistry()->unregisterStat(&d_split_lemmas);
smtStatisticsRegistry()->unregisterStat(&d_disamb_term_lemmas);
- smtStatisticsRegistry()->unregisterStat(&d_sym_break_lemmas);
smtStatisticsRegistry()->unregisterStat(&d_totality_lemmas);
smtStatisticsRegistry()->unregisterStat(&d_max_model_size);
}
namespace CVC4 {
class SortInference;
namespace theory {
-class SubsortSymmetryBreaker;
namespace uf {
class TheoryUF;
} /* namespace CVC4::theory::uf */
~StrongSolverTheoryUF();
/** get theory */
TheoryUF* getTheory() { return d_th; }
- /** symmetry breaker */
- SubsortSymmetryBreaker* getSymmetryBreaker() { return d_sym_break; }
/** get sort inference module */
SortInference* getSortInference();
/** get default sat context */
IntStat d_clique_lemmas;
IntStat d_split_lemmas;
IntStat d_disamb_term_lemmas;
- IntStat d_sym_break_lemmas;
IntStat d_totality_lemmas;
IntStat d_max_model_size;
Statistics();
context::CDO<int> d_min_pos_tn_master_card;
/** relevant eqc */
NodeBoolMap d_rel_eqc;
- /** symmetry breaking techniques */
- SubsortSymmetryBreaker* d_sym_break;
}; /* class StrongSolverTheoryUF */
projects / cvc5.git / commitdiff