mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

remove var-constraint alltogether

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-06-22 20:58:32 -07:00
parent b9719768a0
commit 01c81405af
5 changed files with 0 additions and 99 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/CMakeLists.txt
View file

@ -11,7 +11,6 @@ z3_add_component(polysat
search_state.cpp
solver.cpp
ule_constraint.cpp
var_constraint.cpp
viable.cpp
COMPONENT_DEPENDENCIES
util

1
src/math/polysat/constraint.cpp
View file

@ -16,7 +16,6 @@ Author:
#include "math/polysat/solver.h"
#include "math/polysat/log.h"
#include "math/polysat/log_helper.h"
#include "math/polysat/var_constraint.h"
#include "math/polysat/eq_constraint.h"
#include "math/polysat/ule_constraint.h"

1
src/math/polysat/solver.h
View file

@ -22,7 +22,6 @@ Author:
#include "math/polysat/boolean.h"
#include "math/polysat/constraint.h"
#include "math/polysat/eq_constraint.h"
#include "math/polysat/var_constraint.h"
#include "math/polysat/ule_constraint.h"
#include "math/polysat/justification.h"
#include "math/polysat/linear_solver.h"

48
src/math/polysat/var_constraint.cpp
View file

@ -1,48 +0,0 @@
/*++
Copyright (c) 2021 Microsoft Corporation
Module Name:
polysat var_constraint
Author:
Nikolaj Bjorner (nbjorner) 2021-03-19
Jakob Rath 2021-04-6
--*/
#if 0
#include "math/polysat/var_constraint.h"
#include "math/polysat/solver.h"
namespace polysat {
std::ostream& var_constraint::display(std::ostream& out) const {
out << "v" << m_var << ": " << m_viable << "\n";
return display_extra(out);
}
constraint_ref var_constraint::resolve(solver& s, pvar v) {
UNREACHABLE();
return nullptr;
}
bool var_constraint::is_always_false() {
return false;
}
bool var_constraint::is_currently_false(solver& s) {
return s.m_vble.is_false(m_var);
}
bool var_constraint::is_currently_true(solver& s) {
return !is_currently_false(s);
}
void var_constraint::narrow(solver& s) {
s.m_vble.intersect_viable(m_var, m_viable);
}
}
#endif

48
src/math/polysat/var_constraint.h
View file

@ -1,48 +0,0 @@
/*++
Copyright (c) 2021 Microsoft Corporation
Module Name:
polysat var_constraint
Abstract:
Var constraints restrict viable values.
The main way var-constraints interact with the solver is to
narrow m_viable during initialization.
Author:
Nikolaj Bjorner (nbjorner) 2021-03-19
Jakob Rath 2021-04-6
--*/
#if 0
// to remove
#pragma once
#include "math/dd/dd_bdd.h"
#include "math/polysat/constraint.h"
namespace polysat {
class var_constraint : public constraint {
pvar m_var;
bdd m_viable;
public:
var_constraint(constraint_manager& m, unsigned lvl, csign_t sign, pvar v, bdd const & b, p_dependency_ref const& dep):
constraint(m, lvl, sign, dep, ckind_t::bit_t), m_var(v), m_viable(b) {}
~var_constraint() override {}
std::ostream& display(std::ostream& out) const override;
constraint_ref resolve(solver& s, pvar v) override;
void narrow(solver& s) override;
bool is_always_false() override;
bool is_currently_false(solver& s) override;
bool is_currently_true(solver& s) override;
};
}
#endif