}
}
-void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ) {
- //make sure internal representatives currently exist
- for( std::map< TypeNode, std::vector< Node > >::iterator it = reps.begin(); it != reps.end(); ++it ){
- if( it->first.isSort() ){
- for( unsigned i=0; i<it->second.size(); i++ ){
- Node r = getInternalRepresentative( it->second[i], Node::null(), 0 );
- }
- }
- }
- Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl;
- for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
- for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
- Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl;
- }
- }
- //store representatives for newly created terms
- std::map< Node, Node > temp_rep_map;
-
- bool success;
- do {
- success = false;
- for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
- for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
- if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){
- Node ni = it->second;
- std::vector< Node > cc;
- cc.push_back( it->second.getOperator() );
- bool changed = false;
- for( unsigned j=0; j<ni.getNumChildren(); j++ ){
- if( ni[j].getType().isSort() ){
- Node r = getRepresentative( ni[j] );
- if( itt->second.find( r )==itt->second.end() ){
- Assert( temp_rep_map.find( r )!=temp_rep_map.end() );
- r = temp_rep_map[r];
- }
- if( r==ni ){
- //found sub-term as instance
- Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl;
- itt->second[it->first] = ni[j];
- changed = false;
- success = true;
- break;
- }else{
- Node ir = itt->second[r];
- cc.push_back( ir );
- if( ni[j]!=ir ){
- changed = true;
- }
- }
- }else{
- changed = false;
- break;
- }
- }
- if( changed ){
- Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc );
- Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl;
- success = true;
- itt->second[it->first] = n;
- temp_rep_map[n] = it->first;
- }
- }
- }
- }
- }while( success );
- Trace("internal-rep-flatten") << "---After flattening : " << std::endl;
- for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
- for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
- Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl;
- }
- }
-}
-
eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){
return d_qe->getActiveEqualityEngine();
}
Node getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache );
/** get score */
int getRepScore( Node n, Node f, int index, TypeNode v_tn );
- /** flatten representatives */
- void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
}; /* EqualityQueryQuantifiersEngine */
}/* CVC4::theory::quantifiers namespace */
int ModelEngine::checkModel(){
FirstOrderModel* fm = d_quantEngine->getModel();
- //flatten the representatives
- //Trace("model-engine-debug") << "Flattening representatives...." << std::endl;
- // d_quantEngine->getEqualityQuery()->flattenRepresentatives(
- // fm->getRepSet()->d_type_reps );
-
//for debugging, setup
for (std::map<TypeNode, std::vector<Node> >::iterator it =
fm->getRepSetPtr()->d_type_reps.begin();
//}
}
-//-------------------------------------------------- handling assertions / eqc
-
-void QuantConflictFind::assertNode( Node q ) {
- /*
- if( d_quantEngine->hasOwnership( q, this ) ){
- Trace("qcf-proc") << "QCF : assertQuantifier : ";
- debugPrintQuant("qcf-proc", q);
- Trace("qcf-proc") << std::endl;
- }
- */
-}
-
-/** new node */
-void QuantConflictFind::newEqClass( Node n ) {
-
-}
-
-/** merge */
-void QuantConflictFind::merge( Node a, Node b ) {
-
-}
-
-/** assert disequal */
-void QuantConflictFind::assertDisequal( Node a, Node b ) {
-
-}
-
//-------------------------------------------------- check function
bool QuantConflictFind::needsCheck( Theory::Effort level ) {
void registerQuantifier(Node q) override;
public:
- /** assert quantifier */
- void assertNode(Node q) override;
- /** new node */
- void newEqClass( Node n );
- /** merge */
- void merge( Node a, Node b );
- /** assert disequal */
- void assertDisequal( Node a, Node b );
/** needs check */
bool needsCheck(Theory::Effort level) override;
/** reset round */
namespace theory {
namespace quantifiers {
-bool QuantifiersRewriter::isClause( Node n ){
- if( isLiteral( n ) ){
- return true;
- }else if( n.getKind()==NOT ){
- return isCube( n[0] );
- }else if( n.getKind()==OR ){
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( !isClause( n[i] ) ){
- return false;
- }
- }
- return true;
- }else if( n.getKind()==IMPLIES ){
- return isCube( n[0] ) && isClause( n[1] );
- }else{
- return false;
- }
-}
-
bool QuantifiersRewriter::isLiteral( Node n ){
switch( n.getKind() ){
case NOT:
return true;
}
-bool QuantifiersRewriter::isCube( Node n ){
- if( isLiteral( n ) ){
- return true;
- }else if( n.getKind()==NOT ){
- return isClause( n[0] );
- }else if( n.getKind()==AND ){
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( !isCube( n[i] ) ){
- return false;
- }
- }
- return true;
- }else{
- return false;
- }
-}
-
void QuantifiersRewriter::addNodeToOrBuilder( Node n, NodeBuilder<>& t ){
if( n.getKind()==OR ){
for( int i=0; i<(int)n.getNumChildren(); i++ ){
private:
static int getPurifyIdLit2( Node n, std::map< Node, int >& visited );
public:
- static bool isClause( Node n );
static bool isLiteral( Node n );
- static bool isCube( Node n );
private:
static bool addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged );
static void addNodeToOrBuilder( Node n, NodeBuilder<>& t );
}
}
-
- Node TheorySetsRels::mkAnd( std::vector<TNode>& conjunctions ) {
- Assert(conjunctions.size() > 0);
- std::set<TNode> all;
-
- for (unsigned i = 0; i < conjunctions.size(); ++i) {
- TNode t = conjunctions[i];
- if (t.getKind() == kind::AND) {
- for(TNode::iterator child_it = t.begin();
- child_it != t.end(); ++child_it) {
- Assert((*child_it).getKind() != kind::AND);
- all.insert(*child_it);
- }
- }
- else {
- all.insert(t);
- }
- }
- Assert(all.size() > 0);
- if (all.size() == 1) {
- // All the same, or just one
- return conjunctions[0];
- }
-
- NodeBuilder<> conjunction(kind::AND);
- std::set<TNode>::const_iterator it = all.begin();
- std::set<TNode>::const_iterator it_end = all.end();
- while (it != it_end) {
- conjunction << *it;
- ++ it;
- }
-
- return conjunction;
- }/* mkAnd() */
-
void TheorySetsRels::printNodeMap(const char* fst,
const char* snd,
const NodeMap& map)
bool areEqual( Node a, Node b );
Node getRepresentative( Node t );
bool exists( std::vector<Node>&, Node );
- Node mkAnd( std::vector< TNode >& assumptions );
inline void addToMembershipDB( Node, Node, Node );
static void printNodeMap(const char* fst,
const char* snd,
namespace theory {
namespace sets {
-typedef std::set<TNode> Elements;
-typedef std::unordered_map<TNode, Elements, TNodeHashFunction> SettermElementsMap;
-
-struct FlattenedNodeTag {};
-typedef expr::Attribute<FlattenedNodeTag, bool> flattened;
-
-
-/**
- * flattenNode looks for children of same kind, and if found merges
- * them into the parent.
- *
- * It simultaneously handles a couple of other optimizations:
- * - trivialNode - if found during exploration, return that node itself
- * (like in case of OR, if "true" is found, makes sense to replace
- * whole formula with "true")
- * - skipNode - as name suggests, skip them
- * (like in case of OR, you may want to skip any "false" nodes found)
- *
- * Use a null node if you want to ignore any of the optimizations.
- */
-RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode)
-{
- if(n.hasAttribute(flattened()) && n.getAttribute(flattened())) {
- return RewriteResponse(REWRITE_DONE, n);
- }
-
- typedef std::unordered_set<TNode, TNodeHashFunction> node_set;
-
- node_set visited;
- visited.insert(skipNode);
-
- std::vector<TNode> toProcess;
- toProcess.push_back(n);
-
- Kind k = n.getKind();
- typedef std::vector<TNode> ChildList;
- ChildList childList; //TNode should be fine, since 'n' is still there
-
- Debug("sets-rewrite-flatten") << "[sets-rewrite-flatten] " << n << std::endl;
- for (unsigned i = 0; i < toProcess.size(); ++ i) {
- TNode current = toProcess[i];
- Debug("sets-rewrite-flatten") << "[sets-rewrite-flatten] > Processing " << current << std::endl;
- for(unsigned j = 0, j_end = current.getNumChildren(); j < j_end; ++ j) {
- TNode child = current[j];
- if(visited.find(child) != visited.end()) {
- continue;
- } else if(child == trivialNode) {
- return RewriteResponse(REWRITE_DONE, trivialNode);
- } else {
- visited.insert(child);
- if(child.getKind() == k) {
- toProcess.push_back(child);
- } else {
- childList.push_back(child);
- }
- }
- }
- }
- if (childList.size() == 0) return RewriteResponse(REWRITE_DONE, skipNode);
- if (childList.size() == 1) return RewriteResponse(REWRITE_AGAIN, childList[0]);
-
- sort(childList.begin(), childList.end());
-
- /* Make sure we are under number of children possible in a node */
- NodeManager* nodeManager = NodeManager::currentNM();
- static const unsigned MAX_CHILDREN = (1u << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN ) - 1;
- AlwaysAssert(childList.size() < MAX_CHILDREN, "do not support formulas this big");
-
- ChildList::iterator cur = childList.begin(), en = childList.end();
- Node ret = (*cur);
- ++cur;
- while( cur != en ) {
- ret = nodeManager->mkNode(k, ret, *cur);
- ret.setAttribute(flattened(), true);
- ++cur;
- }
- Trace("sets-postrewrite") << "flatten Sets::postRewrite returning " << ret << std::endl;
- if(ret != n) {
- return RewriteResponse(REWRITE_AGAIN, ret); // again for constants
- } else {
- return RewriteResponse(REWRITE_DONE, ret);
- }
- // if (childList.size() < MAX_CHILDREN) {
- // Node retNode = nodeManager->mkNode(k, childList);
- // return RewriteResponse(REWRITE_DONE, retNode);
- // } else {
- // Assert(childList.size() < size_t(MAX_CHILDREN) * size_t(MAX_CHILDREN) );
- // NodeBuilder<> nb(k);
- // ChildList::iterator cur = childList.begin(), next, en = childList.end();
- // while( cur != en ) {
- // next = min(cur + MAX_CHILDREN, en);
- // nb << (nodeManager->mkNode(k, ChildList(cur, next) ));
- // cur = next;
- // }
- // return RewriteResponse(REWRITE_DONE, nb.constructNode());
- // }
-}
-
bool checkConstantMembership(TNode elementTerm, TNode setTerm)
{
if(setTerm.getKind() == kind::EMPTYSET) {
default:
break;
- }//switch(node.getKind())
+ }
- // This default implementation
return RewriteResponse(REWRITE_DONE, node);
}
projects / cvc5.git / commitdiff