mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
ensure compilation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
560f072786
commit
731cf9b885
|
@ -37,6 +37,7 @@ endforeach()
|
|||
add_subdirectory(util)
|
||||
add_subdirectory(math/polynomial)
|
||||
add_subdirectory(math/dd)
|
||||
add_subdirectory(math/polysat)
|
||||
add_subdirectory(math/hilbert)
|
||||
add_subdirectory(math/simplex)
|
||||
add_subdirectory(math/automata)
|
||||
|
|
7
src/math/polysat/CMakeLists.txt
Normal file
7
src/math/polysat/CMakeLists.txt
Normal file
|
@ -0,0 +1,7 @@
|
|||
z3_add_component(polysat
|
||||
SOURCES
|
||||
polysat.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
util
|
||||
dd
|
||||
)
|
94
src/math/polysat/polysat.cpp
Normal file
94
src/math/polysat/polysat.cpp
Normal file
|
@ -0,0 +1,94 @@
|
|||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
polysat
|
||||
|
||||
Abstract:
|
||||
|
||||
Polynomial solver for modular arithmetic.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
|
||||
--*/
|
||||
|
||||
#include "math/polysat/polysat.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
std::ostream& poly::display(std::ostream& out) const {
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& constraint::display(std::ostream& out) const {
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& linear::display(std::ostream& out) const {
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& mono::display(std::ostream& out) const {
|
||||
return out;
|
||||
}
|
||||
|
||||
unsigned solver::poly2size(poly const& p) const {
|
||||
return 0;
|
||||
}
|
||||
|
||||
bool solver::is_viable(unsigned var, rational const& val) const {
|
||||
return false;
|
||||
}
|
||||
|
||||
/*
|
||||
struct del_var;
|
||||
struct del_constraint;
|
||||
struct var_unassign;
|
||||
|
||||
void push();
|
||||
void pop(unsigned n);
|
||||
|
||||
solver(trail_stack& s);
|
||||
~solver() {}
|
||||
|
||||
lbool check_sat();
|
||||
|
||||
unsigned add_var(unsigned sz);
|
||||
|
||||
poly var(unsigned v);
|
||||
poly mul(rational cons& r, poly const& p);
|
||||
poly num(rational const& r, unsigned sz);
|
||||
poly add(poly const& p, poly const& q);
|
||||
|
||||
vector<mono> poly2monos(poly const& p) const;
|
||||
|
||||
void add_eq(poly const& p, unsigned dep);
|
||||
void add_diseq(poly const& p, unsigned dep);
|
||||
void add_ule(poly const& p, poly const& q, unsigned dep);
|
||||
void add_sle(poly const& p, poly const& q, unsigned dep);
|
||||
void assign(unsigned var, unsigned index, bool value, unsigned dep);
|
||||
|
||||
bool can_propagate();
|
||||
lbool propagate();
|
||||
|
||||
bool can_decide();
|
||||
void decide(rational & val, unsigned& var);
|
||||
void assign(unsigned var, rational const& val);
|
||||
|
||||
bool is_conflict();
|
||||
unsigned resolve_conflict(unsigned_vector& deps);
|
||||
|
||||
bool can_learn();
|
||||
void learn(constraint& c, unsigned_vector& deps);
|
||||
void learn(vector<constraint>& cs, unsigned_vector& deps);
|
||||
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
|
||||
*/
|
||||
|
||||
}
|
||||
|
||||
|
|
@ -18,12 +18,15 @@ Author:
|
|||
|
||||
#include "util/dependency.h"
|
||||
#include "util/trail.h"
|
||||
#include "util/math/dd_pdd.h"
|
||||
#include "util/math/dd_bdd.h"
|
||||
#include "util/lbool.h"
|
||||
#include "math/dd/dd_pdd.h"
|
||||
#include "math/dd/dd_bdd.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
class solver;
|
||||
typedef dd::pdd pdd;
|
||||
typedef dd::bdd bdd;
|
||||
|
||||
class poly {
|
||||
solver& s;
|
||||
|
@ -35,7 +38,7 @@ namespace polysat {
|
|||
std::ostream& display(std::ostream& out) const;
|
||||
};
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, poly const& p) { return p.display(p); }
|
||||
inline std::ostream& operator<<(std::ostream& out, poly const& p) { return p.display(out); }
|
||||
|
||||
enum ckind_t { eq_t, ule_t, sle_t };
|
||||
|
||||
|
@ -72,10 +75,10 @@ namespace polysat {
|
|||
/**
|
||||
* monomial is a list of variables and coefficient.
|
||||
*/
|
||||
clas mono : public unsigned_vector {
|
||||
class mono : public unsigned_vector {
|
||||
rational m_coeff;
|
||||
public:
|
||||
linear(rational const& coeff): m_coeff(coeff) {}
|
||||
mono(rational const& coeff): m_coeff(coeff) {}
|
||||
rational const& coeff() const { return m_coeff; }
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
};
|
||||
|
@ -117,10 +120,10 @@ namespace polysat {
|
|||
|
||||
// Per constraint state
|
||||
vector<u_dependency> m_cdeps; // each constraint has set of dependencies
|
||||
vector<constraint> m_constraints
|
||||
vector<constraint> m_constraints;
|
||||
|
||||
// Per variable information
|
||||
vector<dd::bdd> m_viable; // set of viable values.
|
||||
vector<bdd> m_viable; // set of viable values.
|
||||
vector<u_dependency> m_vdeps; // dependencies for viable values
|
||||
vector<vector<poly>> m_pdeps; // dependencies in polynomial form
|
||||
vector<rational> m_value; // assigned value
|
||||
|
@ -176,7 +179,7 @@ namespace polysat {
|
|||
* Create polynomial terms
|
||||
*/
|
||||
poly var(unsigned v);
|
||||
poly mul(rational cons& r, poly const& p);
|
||||
poly mul(rational const& r, poly const& p);
|
||||
poly num(rational const& r, unsigned sz);
|
||||
poly add(poly const& p, poly const& q);
|
||||
|
||||
|
|
Loading…
Reference in a new issue