GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sort_inference.h Lines: 5 6 83.3 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sort_inference.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Paul Meng, Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Pre-process step for performing sort inference
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__SORT_INFERENCE_H
18
#define CVC4__SORT_INFERENCE_H
19
20
#include <map>
21
#include <vector>
22
23
#include "expr/node.h"
24
#include "expr/type_node.h"
25
26
namespace CVC4 {
27
namespace theory {
28
29
/** sort inference
30
 *
31
 * This class implements sort inference techniques, which rewrites a
32
 * formula F into an equisatisfiable formula F', where the symbols g in F are
33
 * replaced by others g', possibly of different types. For details, see e.g.:
34
 *   "Sort it out with Monotonicity" Claessen 2011
35
 *   "Non-Cyclic Sorts for First-Order Satisfiability" Korovin 2013.
36
 */
37
class SortInference {
38
private:
39
  //all subsorts
40
  std::vector< int > d_sub_sorts;
41
  std::map< int, bool > d_non_monotonic_sorts;
42
  std::map< TypeNode, std::vector< int > > d_type_sub_sorts;
43
  void recordSubsort( TypeNode tn, int s );
44
public:
45
12
  class UnionFind {
46
  public:
47
12
    UnionFind(){}
48
    UnionFind( UnionFind& c ){
49
      set( c );
50
    }
51
    std::map< int, int > d_eqc;
52
    //pairs that must be disequal
53
    std::vector< std::pair< int, int > > d_deq;
54
    void print(const char * c);
55
12
    void clear() { d_eqc.clear(); d_deq.clear(); }
56
    void set( UnionFind& c );
57
    int getRepresentative( int t );
58
    void setEqual( int t1, int t2 );
59
    void setDisequal( int t1, int t2 ){ d_deq.push_back( std::pair< int, int >( t1, t2 ) ); }
60
    bool areEqual( int t1, int t2 ) { return getRepresentative( t1 )==getRepresentative( t2 ); }
61
    bool isValid();
62
  };
63
64
 private:
65
  /** the id count for all subsorts we have allocated */
66
  int d_sortCount;
67
  UnionFind d_type_union_find;
68
  std::map< int, TypeNode > d_type_types;
69
  std::map< TypeNode, int > d_id_for_types;
70
  //for apply uf operators
71
  std::map< Node, int > d_op_return_types;
72
  std::map< Node, std::vector< int > > d_op_arg_types;
73
  std::map< Node, int > d_equality_types;
74
  //for bound variables
75
  std::map< Node, std::map< Node, int > > d_var_types;
76
  //get representative
77
  void setEqual( int t1, int t2 );
78
  int getIdForType( TypeNode tn );
79
  void printSort( const char* c, int t );
80
  //process
81
  int process( Node n, std::map< Node, Node >& var_bound, std::map< Node, int >& visited );
82
  // for monotonicity inference
83
 private:
84
  void processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound, std::map< Node, std::map< int, bool > >& visited, bool typeMode = false );
85
86
//for rewriting
87
private:
88
  //mapping from old symbols to new symbols
89
  std::map< Node, Node > d_symbol_map;
90
  //mapping from constants to new symbols
91
  std::map< TypeNode, std::map< Node, Node > > d_const_map;
92
  //helper functions for simplify
93
  TypeNode getOrCreateTypeForId( int t, TypeNode pref );
94
  TypeNode getTypeForId( int t );
95
  Node getNewSymbol( Node old, TypeNode tn );
96
  //simplify
97
  Node simplifyNode(Node n,
98
                    std::map<Node, Node>& var_bound,
99
                    TypeNode tnn,
100
                    std::map<Node, Node>& model_replace_f,
101
                    std::map<Node, std::map<TypeNode, Node> >& visited);
102
  //make injection
103
  Node mkInjection( TypeNode tn1, TypeNode tn2 );
104
  //reset
105
  void reset();
106
107
 public:
108
12
  SortInference() : d_sortCount(1) {}
109
12
  ~SortInference(){}
110
111
  /** initialize
112
   *
113
   * This initializes this class. The input formula is indicated by assertions.
114
   */
115
  void initialize(const std::vector<Node>& assertions);
116
  /** simplify
117
   *
118
   * This returns the simplified form of formula n, based on the information
119
   * computed during initialization. The argument model_replace_f stores the
120
   * mapping between functions and their analog in the sort-inferred signature.
121
   * The argument visited is a cache of the internal results of simplifying
122
   * previous nodes with this class.
123
   *
124
   * Must call initialize() before this function.
125
   */
126
  Node simplify(Node n,
127
                std::map<Node, Node>& model_replace_f,
128
                std::map<Node, std::map<TypeNode, Node> >& visited);
129
  /** get new constraints
130
   *
131
   * This adds constraints to new_asserts that ensure the following.
132
   * Let F be the conjunction of assertions from the input. Let F' be the
133
   * conjunction of the simplified form of each conjunct in F. Let C be the
134
   * conjunction of formulas adding to new_asserts. Then, F and F' ^ C are
135
   * equisatisfiable.
136
   */
137
  void getNewAssertions(std::vector<Node>& new_asserts);
138
  /** compute monotonicity
139
   *
140
   * This computes whether sorts are monotonic (see e.g. Claessen 2011). If
141
   * this function is called, then calls to isMonotonic() can subsequently be
142
   * used to query whether sorts are monotonic.
143
   */
144
  void computeMonotonicity(const std::vector<Node>& assertions);
145
  /** return true if tn was inferred to be monotonic */
146
  bool isMonotonic(TypeNode tn);
147
  //get sort id for term n
148
  int getSortId( Node n );
149
  //get sort id for variable of quantified formula f
150
  int getSortId( Node f, Node v );
151
  //set that sk is the skolem variable of v for quantifier f
152
  void setSkolemVar( Node f, Node v, Node sk );
153
public:
154
  //is well sorted
155
  bool isWellSortedFormula( Node n );
156
  bool isWellSorted( Node n );
157
private:
158
  // store monotonicity for original sorts as well
159
 std::map<TypeNode, bool> d_non_monotonic_sorts_orig;
160
 /**
161
  * Returns true if k is the APPLY_UF kind and we are not using higher-order
162
  * techniques. This is called in places where we want to know whether to
163
  * treat a term as uninterpreted function.
164
  */
165
 bool isHandledApplyUf(Kind k) const;
166
};
167
168
}  // namespace theory
169
}
170
171
#endif