1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
|
/********************* */
/*! \file iand_solver.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Makai Mann, Gereon Kremer
** This file is part of the CVC4 project.
** Copyright (c) 2009-2021 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 Solver for integer and (IAND) constraints
**/
#ifndef CVC5__THEORY__ARITH__NL__IAND_SOLVER_H
#define CVC5__THEORY__ARITH__NL__IAND_SOLVER_H
#include <map>
#include <vector>
#include "context/cdhashset.h"
#include "expr/node.h"
#include "theory/arith/nl/iand_utils.h"
namespace cvc5 {
namespace theory {
namespace arith {
class ArithState;
class InferenceManager;
namespace nl {
class NlModel;
/** Integer and solver class
*
*/
class IAndSolver
{
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
public:
IAndSolver(InferenceManager& im, ArithState& state, NlModel& model);
~IAndSolver();
/** init last call
*
* This is called at the beginning of last call effort check, where
* assertions are the set of assertions belonging to arithmetic,
* false_asserts is the subset of assertions that are false in the current
* model, and xts is the set of extended function terms that are active in
* the current context.
*/
void initLastCall(const std::vector<Node>& assertions,
const std::vector<Node>& false_asserts,
const std::vector<Node>& xts);
//-------------------------------------------- lemma schemas
/** check initial refine
*
* Returns a set of valid theory lemmas, based on simple facts about IAND.
*
* Examples where iand is shorthand for (_ iand k):
*
* 0 <= iand(x,y) < 2^k
* iand(x,y) <= x
* iand(x,y) <= y
* x=y => iand(x,y)=x
*
* This should be a heuristic incomplete check that only introduces a
* small number of new terms in the lemmas it returns.
*/
void checkInitialRefine();
/** check full refine
*
* This should be a complete check that returns at least one lemma to
* rule out the current model.
*/
void checkFullRefine();
//-------------------------------------------- end lemma schemas
private:
// The inference manager that we push conflicts and lemmas to.
InferenceManager& d_im;
/** Reference to the non-linear model object */
NlModel& d_model;
/** commonly used terms */
Node d_false;
Node d_true;
Node d_zero;
Node d_one;
Node d_two;
IAndUtils d_iandUtils;
/** IAND terms that have been given initial refinement lemmas */
NodeSet d_initRefine;
/** all IAND terms, for each bit-width */
std::map<unsigned, std::vector<Node> > d_iands;
/**
* convert integer value to bitvector value of bitwidth k,
* equivalent to Rewriter::rewrite( ((_ intToBv k) n) ).
*/
Node convertToBvK(unsigned k, Node n) const;
/** make iand */
Node mkIAnd(unsigned k, Node x, Node y) const;
/** make ior */
Node mkIOr(unsigned k, Node x, Node y) const;
/** make inot */
Node mkINot(unsigned k, Node i) const;
/**
* Value-based refinement lemma for i of the form ((_ iand k) x y). Returns:
* x = M(x) ^ y = M(y) =>
* ((_ iand k) x y) = Rewriter::rewrite(((_ iand k) M(x) M(y)))
*/
Node valueBasedLemma(Node i);
/**
* Sum-based refinement lemma for i of the form ((_ iand k) x y). Returns:
* i = 2^0*min(x[0],y[0])+...2^{k-1}*min(x[k-1],y[k-1])
* where x[i] is x div i mod 2
* and min is defined with an ite.
*/
Node sumBasedLemma(Node i);
/** Bitwise refinement lemma for i of the form ((_ iand k) x y). Returns:
* x[j] & y[j] == ite(x[j] == 1 /\ y[j] == 1, 1, 0)
* for all j where M(x)[j] ^ M(y)[j]
* does not match M(((_ iand k) x y))
*/
Node bitwiseLemma(Node i);
}; /* class IAndSolver */
} // namespace nl
} // namespace arith
} // namespace theory
} // namespace cvc5
#endif /* CVC5__THEORY__ARITH__IAND_SOLVER_H */
|
