1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6     nlsat_assignment.h
7 
8 Abstract:
9 
10     Assignment: Var -> Algebraic Number
11 
12 Author:
13 
14     Leonardo de Moura (leonardo) 2012-01-08.
15 
16 Revision History:
17 
18 --*/
19 #pragma once
20 
21 #include "nlsat/nlsat_types.h"
22 #include "math/polynomial/algebraic_numbers.h"
23 
24 namespace nlsat {
25 
26     /**
27        \brief A mapping from variables to values.
28        This mapping is used to encode the current partial interpretation in nlsat.
29     */
30     class assignment : public polynomial::var2anum {
31         scoped_anum_vector m_values;
32         bool_vector      m_assigned;
33     public:
assignment(anum_manager & _m)34         assignment(anum_manager & _m):m_values(_m) {}
~assignment()35         virtual ~assignment() {}
am()36         anum_manager & am() const { return m_values.m(); }
swap(assignment & other)37         void swap(assignment & other) {
38             m_values.swap(other.m_values);
39             m_assigned.swap(other.m_assigned);
40         }
copy(assignment const & other)41         void copy(assignment const& other) {
42             m_assigned.reset();
43             m_assigned.append(other.m_assigned);
44             m_values.reserve(m_assigned.size(), anum());
45             for (unsigned i = 0; i < m_assigned.size(); ++i) {
46                 if (is_assigned(i)) {
47                     am().set(m_values[i], other.value(i));
48                 }
49             }
50         }
51 
set_core(var x,anum & v)52         void set_core(var x, anum & v) {
53             m_values.reserve(x+1, anum());
54             m_assigned.reserve(x+1, false);
55             m_assigned[x] = true;
56             am().swap(m_values[x], v);
57         }
set(var x,anum const & v)58         void set(var x, anum const & v) {
59             m_values.reserve(x+1, anum());
60             m_assigned.reserve(x+1, false);
61             m_assigned[x] = true;
62             am().set(m_values[x], v);
63         }
reset(var x)64         void reset(var x) { if (x < m_assigned.size()) m_assigned[x] = false; }
reset()65         void reset() { m_assigned.reset(); }
is_assigned(var x)66         bool is_assigned(var x) const { return m_assigned.get(x, false); }
value(var x)67         anum const & value(var x) const { return m_values[x]; }
m()68         anum_manager & m() const override { return am(); }
contains(var x)69         bool contains(var x) const override { return is_assigned(x); }
operator()70         anum const & operator()(var x) const override { SASSERT(is_assigned(x)); return value(x); }
swap(var x,var y)71         void swap(var x, var y) {
72             SASSERT(x < m_values.size() && y < m_values.size());
73             std::swap(m_assigned[x], m_assigned[y]);
74             std::swap(m_values[x], m_values[y]);
75         }
display(std::ostream & out)76         void display(std::ostream& out) const {
77             for (unsigned i = 0; i < m_assigned.size(); ++i) {
78                 if (m_assigned[i]) {
79                     out << "x" << i << " := ";
80                     m_values.m().display(out, m_values[i]);
81                     out << "\n";
82                 }
83             }
84         }
85     };
86 
87     /**
88        \brief Wrapper for temporarily unassigning a given variable y.
89        That is, given an assignment M, M' = undef_var_assignment(M, y) is identical
90        to M, but y is unassigned in M'
91     */
92     class undef_var_assignment : public polynomial::var2anum {
93         assignment const & m_assignment;
94         var                m_y;
95     public:
undef_var_assignment(assignment const & a,var y)96         undef_var_assignment(assignment const & a, var y):m_assignment(a), m_y(y) {}
m()97         anum_manager & m() const override { return m_assignment.am(); }
contains(var x)98         bool contains(var x) const override { return x != m_y && m_assignment.is_assigned(x); }
operator()99         anum const & operator()(var x) const override { return m_assignment.value(x); }
100     };
101 };
102 
103