diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-09-27 09:27:19 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-09-27 09:27:29 -0500 |
commit | e277b4d220a1d15ac32f6e4fc5f06e88f55b7f68 (patch) | |
tree | 2a56691dea81453e5f9ba42e859fdc6783fa1545 /src/theory/quantifiers/symmetry_breaking.h | |
parent | ccd1ca4c32e8a3eac8b18911a7b2d32b55203707 (diff) |
Add new symmetry breaking technique for finite model finding. Improvements to bounded integer quantifier instantiation.
Diffstat (limited to 'src/theory/quantifiers/symmetry_breaking.h')
-rwxr-xr-x | src/theory/quantifiers/symmetry_breaking.h | 121 |
1 files changed, 121 insertions, 0 deletions
diff --git a/src/theory/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h new file mode 100755 index 000000000..3db9097f5 --- /dev/null +++ b/src/theory/quantifiers/symmetry_breaking.h @@ -0,0 +1,121 @@ +/********************* */ +/*! \file symmetry_breaking.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** 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 "theory/theory.h" + +#include <iostream> +#include <string> +#include <vector> +#include <map> +#include "expr/node.h" +#include "expr/type_node.h" + +#include "util/sort_inference.h" +#include "context/context.h" +#include "context/context_mm.h" +#include "context/cdchunk_list.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::CDChunkList<int> IntList; + typedef context::CDList<Node> NodeList; + typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap; +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 { + private: + SubsortSymmetryBreaker * d_ssb; + //bool isActive( Node n, unsigned & deq ); + public: + TypeInfo( SubsortSymmetryBreaker * ssb, 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(); + }; + 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; + + TypeInfo * getTypeInfo( 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 ); + /** 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 ); +}; + +} +} + +#endif |