mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 19:35:50 +00:00
Merge branch 'master' of https://github.com/z3prover/z3
This commit is contained in:
Nikolaj Bjorner
commit
b8680f8a46
50 changed files with 131 additions and 131 deletions
|
|
@ -427,11 +427,11 @@ Version 3.0
|
|||
|
||||
- New Bitvector (QF_BV) solver. The new solver is only available when using the new SMT2 front-end.
|
||||
|
||||
- Major performace improvements.
|
||||
- Major performance improvements.
|
||||
|
||||
- New preprocessing stack.
|
||||
|
||||
- Performance improvements for linear and nonlinear arithmetic. The improvements are only available when using the the SMT2 front-end.
|
||||
- Performance improvements for linear and nonlinear arithmetic. The improvements are only available when using the SMT2 front-end.
|
||||
|
||||
- Added API for parsing SMT2 files.
|
||||
|
||||
|
|
@ -772,7 +772,7 @@ This release also introduces some new preprocessing features:
|
|||
|
||||
- More efficient destructive equality resolution DER=true.
|
||||
|
||||
- DISTRIBUTE_FORALL=true (distributes universal quatifiers over conjunctions, this transformation may affect pattern inference).
|
||||
- DISTRIBUTE_FORALL=true (distributes universal quantifiers over conjunctions, this transformation may affect pattern inference).
|
||||
|
||||
- Rewriter that uses universally quantified equations PRE_DEMODULATOR=true (yes, the option name is not good, we will change it in a future release).
|
||||
|
||||
|
|
@ -842,7 +842,7 @@ This release introduces the following features:
|
|||
|
||||
It fixes the following bugs:
|
||||
|
||||
- Incorrect simplification of map over store in the extendted array theory. Reported by Catalin Hritcu.
|
||||
- Incorrect simplification of map over store in the extended array theory. Reported by Catalin Hritcu.
|
||||
|
||||
- Incomplete handling of equality propagation with constant arrays. Reported by Catalin Hritcu.
|
||||
|
||||
|
|
@ -886,7 +886,7 @@ Version 2.0
|
|||
proof object.
|
||||
|
||||
- Proof Objects.
|
||||
The #Z3_check_assumptions retuns a proof object if
|
||||
The #Z3_check_assumptions returns a proof object if
|
||||
the configuration flag PROOF_MODE is set to 1 or 2.
|
||||
|
||||
- Partial support for non-linear arithmetic.
|
||||
|
|
@ -899,4 +899,4 @@ Version 2.0
|
|||
The theory of well-founded recursive data-types is supported
|
||||
over the binary APIs. It supports ground satisfiability checking
|
||||
for tuples, enumeration types (scalars),
|
||||
lists and mututally recursive data-types.
|
||||
lists and mutually recursive data-types.
|
||||
|
|
|
|||
|
|
@ -51,7 +51,7 @@ namespace api {
|
|||
class context : public tactic_manager {
|
||||
struct add_plugins { add_plugins(ast_manager & m); };
|
||||
context_params m_params;
|
||||
bool m_user_ref_count; //!< if true, the user is responsible for managing referenc counters.
|
||||
bool m_user_ref_count; //!< if true, the user is responsible for managing reference counters.
|
||||
scoped_ptr<ast_manager> m_manager;
|
||||
add_plugins m_plugins;
|
||||
|
||||
|
|
@ -158,7 +158,7 @@ namespace api {
|
|||
// Create a numeral of the given sort
|
||||
expr * mk_numeral_core(rational const & n, sort * s);
|
||||
|
||||
// Return a conjuction that will be exposed to the "external" world.
|
||||
// Return a conjunction that will be exposed to the "external" world.
|
||||
expr * mk_and(unsigned num_exprs, expr * const * exprs);
|
||||
|
||||
// Hack for preventing an AST for being GC when ref-count is not used
|
||||
|
|
|
|||
|
|
@ -187,8 +187,8 @@ namespace z3 {
|
|||
\brief The C++ API uses by defaults exceptions on errors.
|
||||
For applications that don't work well with exceptions (there should be only few)
|
||||
you have the ability to turn off exceptions. The tradeoffs are that applications
|
||||
have to very careful about using check_error() after calls that may result in an errornous
|
||||
state.
|
||||
have to very careful about using check_error() after calls that may result in an
|
||||
erroneous state.
|
||||
*/
|
||||
void set_enable_exceptions(bool f) { m_enable_exceptions = f; }
|
||||
|
||||
|
|
@ -213,7 +213,7 @@ namespace z3 {
|
|||
|
||||
/**
|
||||
\brief Interrupt the current procedure being executed by any object managed by this context.
|
||||
This is a soft interruption: there is no guarantee the object will actualy stop.
|
||||
This is a soft interruption: there is no guarantee the object will actually stop.
|
||||
*/
|
||||
void interrupt() { Z3_interrupt(m_ctx); }
|
||||
|
||||
|
|
@ -709,7 +709,7 @@ namespace z3 {
|
|||
|
||||
It only makes sense to use this function if the caller can ensure that
|
||||
the result is an integer or if exceptions are enabled.
|
||||
If exceptions are disabled, then use the the is_numeral_i function.
|
||||
If exceptions are disabled, then use the is_numeral_i function.
|
||||
|
||||
\pre is_numeral()
|
||||
*/
|
||||
|
|
@ -729,7 +729,7 @@ namespace z3 {
|
|||
|
||||
It only makes sense to use this function if the caller can ensure that
|
||||
the result is an integer or if exceptions are enabled.
|
||||
If exceptions are disabled, then use the the is_numeral_u function.
|
||||
If exceptions are disabled, then use the is_numeral_u function.
|
||||
\pre is_numeral()
|
||||
*/
|
||||
unsigned get_numeral_uint() const {
|
||||
|
|
|
|||
|
|
@ -56,7 +56,7 @@ namespace Microsoft.Z3
|
|||
public bool IsDouble { get { return m_is_double; } }
|
||||
|
||||
/// <summary>
|
||||
/// The string representation of the the entry's value.
|
||||
/// The string representation of the entry's value.
|
||||
/// </summary>
|
||||
public string Value
|
||||
{
|
||||
|
|
|
|||
|
|
@ -934,7 +934,7 @@ public class Context implements AutoCloseable {
|
|||
* exposed. It follows the semantics prescribed by the SMT-LIB standard.
|
||||
*
|
||||
* You can take the floor of a real by creating an auxiliary integer Term
|
||||
* {@code k} and and asserting
|
||||
* {@code k} and asserting
|
||||
* {@code MakeInt2Real(k) <= t1 < MkInt2Real(k)+1}. The argument
|
||||
* must be of integer sort.
|
||||
**/
|
||||
|
|
|
|||
|
|
@ -65,7 +65,7 @@ public class Statistics extends Z3Object {
|
|||
}
|
||||
|
||||
/**
|
||||
* The string representation of the the entry's value.
|
||||
* The string representation of the entry's value.
|
||||
*
|
||||
* @throws Z3Exception
|
||||
**/
|
||||
|
|
|
|||
|
|
@ -5741,7 +5741,7 @@ class ModelRef(Z3PPObject):
|
|||
return None
|
||||
|
||||
def num_sorts(self):
|
||||
"""Return the number of unintepreted sorts that contain an interpretation in the model `self`.
|
||||
"""Return the number of uninterpreted sorts that contain an interpretation in the model `self`.
|
||||
|
||||
>>> A = DeclareSort('A')
|
||||
>>> a, b = Consts('a b', A)
|
||||
|
|
@ -5756,7 +5756,7 @@ class ModelRef(Z3PPObject):
|
|||
return int(Z3_model_get_num_sorts(self.ctx.ref(), self.model))
|
||||
|
||||
def get_sort(self, idx):
|
||||
"""Return the unintepreted sort at position `idx` < self.num_sorts().
|
||||
"""Return the uninterpreted sort at position `idx` < self.num_sorts().
|
||||
|
||||
>>> A = DeclareSort('A')
|
||||
>>> B = DeclareSort('B')
|
||||
|
|
@ -5796,7 +5796,7 @@ class ModelRef(Z3PPObject):
|
|||
return [ self.get_sort(i) for i in range(self.num_sorts()) ]
|
||||
|
||||
def get_universe(self, s):
|
||||
"""Return the intepretation for the uninterpreted sort `s` in the model `self`.
|
||||
"""Return the interpretation for the uninterpreted sort `s` in the model `self`.
|
||||
|
||||
>>> A = DeclareSort('A')
|
||||
>>> a, b = Consts('a b', A)
|
||||
|
|
@ -5816,7 +5816,7 @@ class ModelRef(Z3PPObject):
|
|||
return None
|
||||
|
||||
def __getitem__(self, idx):
|
||||
"""If `idx` is an integer, then the declaration at position `idx` in the model `self` is returned. If `idx` is a declaration, then the actual interpreation is returned.
|
||||
"""If `idx` is an integer, then the declaration at position `idx` in the model `self` is returned. If `idx` is a declaration, then the actual interpretation is returned.
|
||||
|
||||
The elements can be retrieved using position or the actual declaration.
|
||||
|
||||
|
|
@ -5860,7 +5860,7 @@ class ModelRef(Z3PPObject):
|
|||
return None
|
||||
|
||||
def decls(self):
|
||||
"""Return a list with all symbols that have an interpreation in the model `self`.
|
||||
"""Return a list with all symbols that have an interpretation in the model `self`.
|
||||
>>> f = Function('f', IntSort(), IntSort())
|
||||
>>> x = Int('x')
|
||||
>>> s = Solver()
|
||||
|
|
|
|||
|
|
@ -363,7 +363,7 @@ extern "C" {
|
|||
void Z3_API Z3_fixedpoint_set_reduce_assign_callback(
|
||||
Z3_context c ,Z3_fixedpoint d, Z3_fixedpoint_reduce_assign_callback_fptr cb);
|
||||
|
||||
/** \brief Register a callback for buildling terms based on the relational operators. */
|
||||
/** \brief Register a callback for building terms based on the relational operators. */
|
||||
void Z3_API Z3_fixedpoint_set_reduce_app_callback(
|
||||
Z3_context c, Z3_fixedpoint d, Z3_fixedpoint_reduce_app_callback_fptr cb);
|
||||
|
||||
|
|
|
|||
|
|
@ -433,7 +433,7 @@ extern "C" {
|
|||
\param c logical context
|
||||
\param rm term of RoundingMode sort
|
||||
\param t1 term of FloatingPoint sort
|
||||
\param t2 term of FloatingPoint sor
|
||||
\param t2 term of FloatingPoint sort
|
||||
\param t3 term of FloatingPoint sort
|
||||
|
||||
The result is round((t1 * t2) + t3)
|
||||
|
|
|
|||
|
|
@ -151,7 +151,7 @@ namespace format_ns {
|
|||
}
|
||||
|
||||
format * mk_int(ast_manager & m, int i) {
|
||||
static char buffer[128];
|
||||
char buffer[128];
|
||||
#ifdef _WINDOWS
|
||||
sprintf_s(buffer, ARRAYSIZE(buffer), "%d", i);
|
||||
#else
|
||||
|
|
@ -161,7 +161,7 @@ namespace format_ns {
|
|||
}
|
||||
|
||||
format * mk_unsigned(ast_manager & m, unsigned u) {
|
||||
static char buffer[128];
|
||||
char buffer[128];
|
||||
#ifdef _WINDOWS
|
||||
sprintf_s(buffer, ARRAYSIZE(buffer), "%u", u);
|
||||
#else
|
||||
|
|
|
|||
|
|
@ -83,7 +83,7 @@ class reduce_hypotheses {
|
|||
// map from unit literals to their hypotheses-free derivations
|
||||
obj_map<expr, proof*> m_units;
|
||||
|
||||
// -- all hypotheses in the the proof
|
||||
// -- all hypotheses in the proof
|
||||
obj_hashtable<expr> m_hyps;
|
||||
|
||||
// marks hypothetical proofs
|
||||
|
|
@ -192,7 +192,7 @@ class reduce_hypotheses {
|
|||
res = mk_lemma_core(args.get(0), m.get_fact(p));
|
||||
compute_mark1(res);
|
||||
} else if (m.is_unit_resolution(p)) {
|
||||
// unit: reduce untis; reduce the first premise; rebuild unit resolution
|
||||
// unit: reduce units; reduce the first premise; rebuild unit resolution
|
||||
res = mk_unit_resolution_core(args.size(), args.c_ptr());
|
||||
compute_mark1(res);
|
||||
} else {
|
||||
|
|
@ -340,7 +340,7 @@ void reduce_hypotheses(proof_ref &pr) {
|
|||
class reduce_hypotheses0 {
|
||||
typedef obj_hashtable<expr> expr_set;
|
||||
ast_manager& m;
|
||||
// reference for any expression created by the tranformation
|
||||
// reference for any expression created by the transformation
|
||||
expr_ref_vector m_refs;
|
||||
// currently computed result
|
||||
obj_map<proof,proof*> m_cache;
|
||||
|
|
@ -352,7 +352,7 @@ class reduce_hypotheses0 {
|
|||
unsigned_vector m_limits;
|
||||
// map from proofs to active hypotheses
|
||||
obj_map<proof, expr_set*> m_hypmap;
|
||||
// refernce train for hypotheses sets
|
||||
// reference train for hypotheses sets
|
||||
ptr_vector<expr_set> m_hyprefs;
|
||||
ptr_vector<expr> m_literals;
|
||||
|
||||
|
|
@ -492,7 +492,7 @@ public:
|
|||
// replace result by m_units[m.get_fact (p)] if defined
|
||||
// AG: This is the main step. Replace a hypothesis by a derivation of its consequence
|
||||
if (!m_units.find(m.get_fact(p), result)) {
|
||||
// restore ther result back to p
|
||||
// restore the result back to p
|
||||
result = p.get();
|
||||
}
|
||||
// compute hypothesis of the result
|
||||
|
|
|
|||
|
|
@ -88,7 +88,7 @@ class elim_aux_assertions {
|
|||
|
||||
app_ref m_aux;
|
||||
public:
|
||||
elim_aux_assertions(app_ref aux) : m_aux(aux) {}
|
||||
elim_aux_assertions(app_ref const& aux) : m_aux(aux) {}
|
||||
|
||||
void mk_or_core(expr_ref_vector &args, expr_ref &res)
|
||||
{
|
||||
|
|
|
|||
|
|
@ -761,7 +761,7 @@ public:
|
|||
return m_array_fid;
|
||||
}
|
||||
virtual char const * get_usage() const { return "<symbol> (<sort>+) <func-decl-ref>"; }
|
||||
virtual char const * get_descr(cmd_context & ctx) const { return "declare a new array map operator with name <symbol> using the given function declaration.\n<func-decl-ref> ::= <symbol>\n | (<symbol> (<sort>*) <sort>)\n | ((_ <symbol> <numeral>+) (<sort>*) <sort>)\nThe last two cases are used to disumbiguate between declarations with the same name and/or select (indexed) builtin declarations.\nFor more details about the the array map operator, see 'Generalized and Efficient Array Decision Procedures' (FMCAD 2009).\nExample: (declare-map set-union (Int) (or (Bool Bool) Bool))\nDeclares a new function (declare-fun set-union ((Array Int Bool) (Array Int Bool)) (Array Int Bool)).\nThe instance of the map axiom for this new declaration is:\n(forall ((a1 (Array Int Bool)) (a2 (Array Int Bool)) (i Int)) (= (select (set-union a1 a2) i) (or (select a1 i) (select a2 i))))"; }
|
||||
virtual char const * get_descr(cmd_context & ctx) const { return "declare a new array map operator with name <symbol> using the given function declaration.\n<func-decl-ref> ::= <symbol>\n | (<symbol> (<sort>*) <sort>)\n | ((_ <symbol> <numeral>+) (<sort>*) <sort>)\nThe last two cases are used to disumbiguate between declarations with the same name and/or select (indexed) builtin declarations.\nFor more details about the array map operator, see 'Generalized and Efficient Array Decision Procedures' (FMCAD 2009).\nExample: (declare-map set-union (Int) (or (Bool Bool) Bool))\nDeclares a new function (declare-fun set-union ((Array Int Bool) (Array Int Bool)) (Array Int Bool)).\nThe instance of the map axiom for this new declaration is:\n(forall ((a1 (Array Int Bool)) (a2 (Array Int Bool)) (i Int)) (= (select (set-union a1 a2) i) (or (select a1 i) (select a2 i))))"; }
|
||||
virtual unsigned get_arity() const { return 3; }
|
||||
virtual void prepare(cmd_context & ctx) { m_name = symbol::null; m_domain.reset(); }
|
||||
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
|
||||
|
|
|
|||
|
|
@ -125,7 +125,7 @@ class stream_ref {
|
|||
std::ostream * m_stream;
|
||||
bool m_owner;
|
||||
public:
|
||||
stream_ref(std::string n, std::ostream & d):m_default_name(n), m_default(d), m_name(n), m_stream(&d), m_owner(false) {}
|
||||
stream_ref(const std::string& n, std::ostream & d):m_default_name(n), m_default(d), m_name(n), m_stream(&d), m_owner(false) {}
|
||||
~stream_ref() { reset(); }
|
||||
void set(char const * name);
|
||||
void set(std::ostream& strm);
|
||||
|
|
|
|||
|
|
@ -66,7 +66,7 @@ namespace Duality {
|
|||
|
||||
bool is_variable(const Term &t);
|
||||
|
||||
FuncDecl SuffixFuncDecl(Term t, int n);
|
||||
FuncDecl SuffixFuncDecl(const Term &t, int n);
|
||||
|
||||
|
||||
Term SubstRecHide(hash_map<ast, Term> &memo, const Term &t, int number);
|
||||
|
|
|
|||
|
|
@ -2157,7 +2157,7 @@ namespace Duality {
|
|||
std::vector<Term> la_pos_vars;
|
||||
bool fixing;
|
||||
|
||||
void IndexLAcoeff(const Term &coeff1, const Term &coeff2, Term t, int id) {
|
||||
void IndexLAcoeff(const Term &coeff1, const Term &coeff2, const Term &t, int id) {
|
||||
Term coeff = coeff1 * coeff2;
|
||||
coeff = coeff.simplify();
|
||||
Term is_pos = (coeff >= ctx.int_val(0));
|
||||
|
|
@ -3303,7 +3303,7 @@ namespace Duality {
|
|||
// This returns a new FuncDel with same sort as top-level function
|
||||
// of term t, but with numeric suffix appended to name.
|
||||
|
||||
Z3User::FuncDecl Z3User::SuffixFuncDecl(Term t, int n)
|
||||
Z3User::FuncDecl Z3User::SuffixFuncDecl(const Term &t, int n)
|
||||
{
|
||||
std::string name = t.decl().name().str() + "_" + string_of_int(n);
|
||||
std::vector<sort> sorts;
|
||||
|
|
|
|||
|
|
@ -107,14 +107,14 @@ namespace Duality {
|
|||
|
||||
struct InternalError {
|
||||
std::string msg;
|
||||
InternalError(const std::string _msg)
|
||||
InternalError(const std::string & _msg)
|
||||
: msg(_msg) {}
|
||||
};
|
||||
|
||||
|
||||
/** This is the main solver. It takes anarbitrary (possibly cyclic)
|
||||
/** This is the main solver. It takes an arbitrary (possibly cyclic)
|
||||
RPFP and either annotates it with a solution, or returns a
|
||||
counterexample derivation in the form of an embedd RPFP tree. */
|
||||
counterexample derivation in the form of an embedded RPFP tree. */
|
||||
|
||||
class Duality : public Solver {
|
||||
|
||||
|
|
|
|||
|
|
@ -191,7 +191,7 @@ namespace Duality {
|
|||
sort int_sort();
|
||||
sort real_sort();
|
||||
sort bv_sort(unsigned sz);
|
||||
sort array_sort(sort d, sort r);
|
||||
sort array_sort(const sort & d, const sort & r);
|
||||
|
||||
func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range);
|
||||
func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range);
|
||||
|
|
@ -763,11 +763,11 @@ namespace Duality {
|
|||
unsigned size() const;
|
||||
func_decl operator[](unsigned i) const;
|
||||
|
||||
expr get_const_interp(func_decl f) const {
|
||||
expr get_const_interp(const func_decl & f) const {
|
||||
return ctx().cook(m_model->get_const_interp(to_func_decl(f.raw())));
|
||||
}
|
||||
|
||||
func_interp get_func_interp(func_decl f) const {
|
||||
func_interp get_func_interp(const func_decl & f) const {
|
||||
return func_interp(ctx(),m_model->get_func_interp(to_func_decl(f.raw())));
|
||||
}
|
||||
|
||||
|
|
@ -1169,7 +1169,7 @@ namespace Duality {
|
|||
::sort *s = m().mk_sort(m_arith_fid, REAL_SORT);
|
||||
return sort(*this, s);
|
||||
}
|
||||
inline sort context::array_sort(sort d, sort r) {
|
||||
inline sort context::array_sort(const sort & d, const sort & r) {
|
||||
parameter params[2] = { parameter(d), parameter(to_sort(r)) };
|
||||
::sort * s = m().mk_sort(m_array_fid, ARRAY_SORT, 2, params);
|
||||
return sort(*this, s);
|
||||
|
|
@ -1274,11 +1274,11 @@ namespace Duality {
|
|||
class TermTree {
|
||||
public:
|
||||
|
||||
TermTree(expr _term){
|
||||
TermTree(const expr &_term){
|
||||
term = _term;
|
||||
}
|
||||
|
||||
TermTree(expr _term, const std::vector<TermTree *> &_children){
|
||||
TermTree(const expr &_term, const std::vector<TermTree *> &_children){
|
||||
term = _term;
|
||||
children = _children;
|
||||
}
|
||||
|
|
@ -1302,9 +1302,9 @@ namespace Duality {
|
|||
return num;
|
||||
}
|
||||
|
||||
inline void setTerm(expr t){term = t;}
|
||||
inline void setTerm(const expr &t){term = t;}
|
||||
|
||||
inline void addTerm(expr t){terms.push_back(t);}
|
||||
inline void addTerm(const expr &t){terms.push_back(t);}
|
||||
|
||||
inline void setChildren(const std::vector<TermTree *> & _children){
|
||||
children = _children;
|
||||
|
|
|
|||
|
|
@ -233,7 +233,7 @@ namespace polynomial {
|
|||
|
||||
/**
|
||||
\brief Install a "delete polynomial" event handler.
|
||||
The even hanlder is not owned by the polynomial manager.
|
||||
The event handler is not owned by the polynomial manager.
|
||||
If eh = 0, then it uninstall the event handler.
|
||||
*/
|
||||
void add_del_eh(del_eh * eh);
|
||||
|
|
@ -426,7 +426,7 @@ namespace polynomial {
|
|||
polynomial * flip_sign_if_lm_neg(polynomial const * p);
|
||||
|
||||
/**
|
||||
\breif Return the gcd g of p and q.
|
||||
\brief Return the gcd g of p and q.
|
||||
*/
|
||||
void gcd(polynomial const * p, polynomial const * q, polynomial_ref & g);
|
||||
|
||||
|
|
@ -853,7 +853,7 @@ namespace polynomial {
|
|||
void resultant(polynomial const * p, polynomial const * q, var x, polynomial_ref & r);
|
||||
|
||||
/**
|
||||
\brief Stroe in r the discriminant of p with respect to variable x.
|
||||
\brief Store in r the discriminant of p with respect to variable x.
|
||||
discriminant(p, x, r) == resultant(p, derivative(p, x), x, r)
|
||||
*/
|
||||
void discriminant(polynomial const * p, var x, polynomial_ref & r);
|
||||
|
|
@ -959,7 +959,7 @@ namespace polynomial {
|
|||
}
|
||||
|
||||
/**
|
||||
\brief Apply substiution [x -> p/q] in r.
|
||||
\brief Apply substitution [x -> p/q] in r.
|
||||
That is, given r \in Z[x, y_1, .., y_m] return
|
||||
polynomial q^k * r(p/q, y_1, .., y_m), where k is the maximal degree of x in r.
|
||||
*/
|
||||
|
|
|
|||
|
|
@ -152,7 +152,7 @@ public:
|
|||
}
|
||||
|
||||
/**
|
||||
\brief 'Disagonalizes' the matrix using only column operations. The reusling matrix will have -1 at pivot
|
||||
\brief 'Diagonalizes' the matrix using only column operations. The resulting matrix will have -1 at pivot
|
||||
elements. Returns the rank of the null space.
|
||||
*/
|
||||
unsigned diagonalize() {
|
||||
|
|
@ -170,7 +170,7 @@ public:
|
|||
m_column_pivot[j] = i;
|
||||
m_row_pivot[i] = j;
|
||||
|
||||
// found a pivot, to make it -1 we compute the multuplier -p^-1
|
||||
// found a pivot, to make it -1 we compute the multiplier -p^-1
|
||||
m_zpm.set(multiplier, get(i, j));
|
||||
m_zpm.inv(multiplier);
|
||||
m_zpm.neg(multiplier);
|
||||
|
|
@ -201,7 +201,7 @@ public:
|
|||
}
|
||||
|
||||
/**
|
||||
If rank of the matrix is n - r, we are interested in linearly indeprendent vectors v_1, ..., v_r (the basis of
|
||||
If rank of the matrix is n - r, we are interested in linearly independent vectors v_1, ..., v_r (the basis of
|
||||
the null space), such that v_k A = 0. This method will give one at a time. The method returns true if vector has
|
||||
been computed properly. The first vector [1, 0, ..., 0] is ignored (m_null_row starts from 1).
|
||||
*/
|
||||
|
|
@ -417,7 +417,7 @@ bool zp_factor_square_free_berlekamp(zp_manager & upm, numeral_vector const & f,
|
|||
// construct the berlekamp Q matrix to get the null space
|
||||
berlekamp_matrix Q_I(upm, f);
|
||||
|
||||
// copy the inital polynomial to factors
|
||||
// copy the initial polynomial to factors
|
||||
unsigned first_factor = factors.distinct_factors();
|
||||
factors.push_back(f, 1);
|
||||
|
||||
|
|
@ -473,7 +473,7 @@ bool zp_factor_square_free_berlekamp(zp_manager & upm, numeral_vector const & f,
|
|||
// get the gcd
|
||||
upm.gcd(v_k.size(), v_k.c_ptr(), current_factor.size(), current_factor.c_ptr(), gcd);
|
||||
|
||||
// if the gcd is 1, or the the gcd is f, we just ignroe it
|
||||
// if the gcd is 1, or the gcd is f, we just ignore it
|
||||
if (gcd.size() != 1 && gcd.size() != current_factor.size()) {
|
||||
|
||||
// get the divisor also (no need to normalize the div, both are monic)
|
||||
|
|
@ -568,13 +568,13 @@ bool check_hansel_lift(z_manager & upm, numeral_vector const & C,
|
|||
}
|
||||
|
||||
/**
|
||||
Performs a Hensel lift of A and B in Z_a to Z_b, where p is prime and and a = p^{a_k}, b = p^{b_k},
|
||||
Performs a Hensel lift of A and B in Z_a to Z_b, where p is prime and a = p^{a_k}, b = p^{b_k},
|
||||
r = (a, b), with the following assumptions:
|
||||
|
||||
(1) UA + VB = 1 (mod a)
|
||||
(1) UA + VB = 1 (mod a)
|
||||
(2) C = A*B (mod b)
|
||||
(3) (l(A), r) = 1 (importand in order to divide by A, i.e. to invert l(A))
|
||||
(4) deg(A) + deg(B) = deg(C)
|
||||
(3) (l(A), r) = 1 (important in order to divide by A, i.e. to invert l(A))
|
||||
(4) deg(A) + deg(B) = deg(C)
|
||||
|
||||
The output of is two polynomials A1, B1 such that A1 = A (mod b), B1 = B (mod b),
|
||||
l(A1) = l(A), deg(A1) = deg(A), deg(B1) = deg(B) and C = A1 B1 (mod b*r). Such A1, B1 are unique if
|
||||
|
|
@ -625,7 +625,7 @@ void hensel_lift(z_manager & upm, numeral const & a, numeral const & b, numeral
|
|||
// having (1) AU + BV = 1 (mod r) and (5) AT + BS = f (mod r), we know that
|
||||
// A*(fU) + B*(fV) = f (mod r), i.e. T = fU, S = fV is a solution
|
||||
// but we also know that we need an S with deg(S) <= deg(A) so we can do the following
|
||||
// we know that l(A) is invertible so we can find the exact remainder of fV with A, i.e. find the qotient
|
||||
// we know that l(A) is invertible so we can find the exact remainder of fV with A, i.e. find the quotient
|
||||
// t in the division and set
|
||||
// A*(fU + tB) + B*(fV - tA) = f
|
||||
// T = fU + tB, S = fU - tA
|
||||
|
|
@ -1093,7 +1093,7 @@ bool factor_square_free(z_manager & upm, numeral_vector const & f, factors & fs,
|
|||
continue;
|
||||
}
|
||||
|
||||
// if it's not square free, we also try somehting else
|
||||
// if it's not square free, we also try something else
|
||||
scoped_numeral_vector f_pp_zp(nm);
|
||||
to_zp_manager(zp_upm, f_pp, f_pp_zp);
|
||||
|
||||
|
|
@ -1170,7 +1170,7 @@ bool factor_square_free(z_manager & upm, numeral_vector const & f, factors & fs,
|
|||
zp_numeral_manager & zpe_nm = zpe_upm.m();
|
||||
|
||||
zp_factors zpe_fs(zpe_upm);
|
||||
// this might give something bigger than p^e, but the lifting proocedure will update the zpe_nm
|
||||
// this might give something bigger than p^e, but the lifting procedure will update the zpe_nm
|
||||
// zp factors are monic, so will be the zpe factors, i.e. f_pp = zpe_fs * lc(f_pp) (mod p^e)
|
||||
hensel_lift(upm, f_pp, zp_fs, e, zpe_fs);
|
||||
|
||||
|
|
@ -1182,7 +1182,7 @@ bool factor_square_free(z_manager & upm, numeral_vector const & f, factors & fs,
|
|||
scoped_numeral f_pp_lc(nm);
|
||||
zpe_nm.set(f_pp_lc, f_pp.back());
|
||||
|
||||
// we always keep in f_pp the the actual primitive part f_pp*lc(f_pp)
|
||||
// we always keep in f_pp the actual primitive part f_pp*lc(f_pp)
|
||||
upm.mul(f_pp, f_pp_lc);
|
||||
|
||||
// now we go through the combinations of factors to check construct the factorization
|
||||
|
|
@ -1287,7 +1287,7 @@ bool factor_square_free(z_manager & upm, numeral_vector const & f, factors & fs,
|
|||
fs.push_back(f_pp, k);
|
||||
}
|
||||
else {
|
||||
// if a constant it must be 1 (it was primitve)
|
||||
// if a constant it must be 1 (it was primitive)
|
||||
SASSERT(f_pp.size() == 1 && nm.is_one(f_pp.back()));
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -34,12 +34,12 @@ namespace upolynomial {
|
|||
typedef manager::scoped_numeral scoped_numeral;
|
||||
|
||||
/**
|
||||
\breif Factor f into f = f_1^k_1 * ... * p_n^k_n, such that p_i are square-free and coprime.
|
||||
\brief Factor f into f = f_1^k_1 * ... * p_n^k_n, such that p_i are square-free and coprime.
|
||||
*/
|
||||
void zp_square_free_factor(zp_manager & zp_upm, numeral_vector const & f, zp_factors & sq_free_factors);
|
||||
|
||||
/**
|
||||
\brief Factor the monic square-free polynomial f from Z_p[x]. Returns true if factorization was sucesseful, or false
|
||||
\brief Factor the monic square-free polynomial f from Z_p[x]. Returns true if factorization was successful, or false
|
||||
if f is an irreducible square-free polynomial in Z_p[x].
|
||||
*/
|
||||
bool zp_factor_square_free(zp_manager & zp_upm, numeral_vector const & f, zp_factors & factors);
|
||||
|
|
@ -55,17 +55,17 @@ namespace upolynomial {
|
|||
bool zp_factor_square_free_berlekamp(zp_manager & zp_upm, numeral_vector const & f, zp_factors & factors, bool randomized = true);
|
||||
|
||||
/**
|
||||
\brief Factor the polynomial f from Z_p[x]. Returns true if factorization was sucesseful, or false if f is
|
||||
\brief Factor the polynomial f from Z_p[x]. Returns true if factorization was successful, or false if f is
|
||||
an irreducible polynomial in Z_p[x]
|
||||
*/
|
||||
bool zp_factor(zp_manager & zp_upm, numeral_vector const & f, zp_factors & factors);
|
||||
|
||||
/**
|
||||
\brief Performs a Hensel lift of A and B in Z_a to Z_b, where p is prime and and a = p^{a_k}, b = p^{b_k},
|
||||
\brief Performs a Hensel lift of A and B in Z_a to Z_b, where p is prime and a = p^{a_k}, b = p^{b_k},
|
||||
r = (a, b), with the following assumptions:
|
||||
* UA + VB = 1 (mod a)
|
||||
* C = AB (mod b)
|
||||
* (l(A), r) = 1 (importand in order to divide by A, i.e. to invert l(A))
|
||||
* (l(A), r) = 1 (important in order to divide by A, i.e. to invert l(A))
|
||||
the output of is two polynomials A1, B1 (replacing A and B) such that A1 = A (mod b), B1 = B (mod b),
|
||||
l(A1) = l(A), deg(A1) = deg(A), deg(B1) = deg(B) and C = A1 B1 (mod b*r). Such A1, B1 are unique if
|
||||
r is prime. See [3] p. 138.
|
||||
|
|
@ -82,7 +82,7 @@ namespace upolynomial {
|
|||
void hensel_lift(z_manager & upm, numeral_vector const & f, zp_factors const & factors_p, unsigned e, zp_factors & factors_pe);
|
||||
|
||||
/**
|
||||
\brief Factor the square-free polynomial f from Z[x]. Returns true if factorization was sucesseful, or false if
|
||||
\brief Factor the square-free polynomial f from Z[x]. Returns true if factorization was successful, or false if
|
||||
f is an irreducible polynomial in Z[x]. The vector of factors is cleared.
|
||||
*/
|
||||
bool factor_square_free(z_manager & upm, numeral_vector const & f, factors & fs, factor_params const & ps = factor_params());
|
||||
|
|
|
|||
|
|
@ -400,7 +400,7 @@ namespace datalog {
|
|||
}
|
||||
uint64 res;
|
||||
if (!try_get_sort_constant_count(srt, res)) {
|
||||
sort_size sz = srt->get_num_elements();
|
||||
const sort_size & sz = srt->get_num_elements();
|
||||
if (sz.is_finite()) {
|
||||
res = sz.size();
|
||||
}
|
||||
|
|
@ -411,7 +411,7 @@ namespace datalog {
|
|||
return res;
|
||||
}
|
||||
|
||||
void context::set_argument_names(const func_decl * pred, svector<symbol> var_names)
|
||||
void context::set_argument_names(const func_decl * pred, const svector<symbol> & var_names)
|
||||
{
|
||||
SASSERT(!m_argument_var_names.contains(pred));
|
||||
m_argument_var_names.insert(pred, var_names);
|
||||
|
|
|
|||
|
|
@ -368,7 +368,7 @@ namespace datalog {
|
|||
These names are used when printing out the relations to make the output conform
|
||||
to the one of bddbddb.
|
||||
*/
|
||||
void set_argument_names(const func_decl * pred, svector<symbol> var_names);
|
||||
void set_argument_names(const func_decl * pred, const svector<symbol> & var_names);
|
||||
symbol get_argument_name(const func_decl * pred, unsigned arg_index);
|
||||
|
||||
void set_predicate_representation(func_decl * pred, unsigned relation_name_cnt,
|
||||
|
|
|
|||
|
|
@ -547,7 +547,7 @@ namespace datalog {
|
|||
//
|
||||
// -----------------------------------
|
||||
|
||||
void get_file_names(std::string directory, std::string extension, bool traverse_subdirs,
|
||||
void get_file_names(std::string directory, const std::string & extension, bool traverse_subdirs,
|
||||
string_vector & res) {
|
||||
|
||||
if(directory[directory.size()-1]!='\\' && directory[directory.size()-1]!='/') {
|
||||
|
|
@ -595,7 +595,7 @@ namespace datalog {
|
|||
#endif
|
||||
}
|
||||
|
||||
bool file_exists(std::string name) {
|
||||
bool file_exists(const std::string & name) {
|
||||
struct stat st;
|
||||
if(stat(name.c_str(),&st) == 0) {
|
||||
return true;
|
||||
|
|
@ -603,7 +603,7 @@ namespace datalog {
|
|||
return false;
|
||||
}
|
||||
|
||||
bool is_directory(std::string name) {
|
||||
bool is_directory(const std::string & name) {
|
||||
if(!file_exists(name)) {
|
||||
return false;
|
||||
}
|
||||
|
|
@ -612,7 +612,7 @@ namespace datalog {
|
|||
return (status.st_mode&S_IFDIR)!=0;
|
||||
}
|
||||
|
||||
std::string get_file_name_without_extension(std::string name) {
|
||||
std::string get_file_name_without_extension(const std::string & name) {
|
||||
size_t slash_index = name.find_last_of("\\/");
|
||||
size_t dot_index = name.rfind('.');
|
||||
size_t ofs = (slash_index==std::string::npos) ? 0 : slash_index+1;
|
||||
|
|
|
|||
|
|
@ -290,7 +290,7 @@ namespace datalog {
|
|||
}
|
||||
|
||||
template<class T>
|
||||
void project_out_vector_columns(T & container, const unsigned_vector removed_cols) {
|
||||
void project_out_vector_columns(T & container, const unsigned_vector & removed_cols) {
|
||||
project_out_vector_columns(container, removed_cols.size(), removed_cols.c_ptr());
|
||||
}
|
||||
|
||||
|
|
@ -342,7 +342,7 @@ namespace datalog {
|
|||
}
|
||||
|
||||
template<class T>
|
||||
void permutate_by_cycle(T & container, const unsigned_vector permutation_cycle) {
|
||||
void permutate_by_cycle(T & container, const unsigned_vector & permutation_cycle) {
|
||||
permutate_by_cycle(container, permutation_cycle.size(), permutation_cycle.c_ptr());
|
||||
}
|
||||
|
||||
|
|
@ -578,13 +578,13 @@ namespace datalog {
|
|||
//
|
||||
// -----------------------------------
|
||||
|
||||
void get_file_names(std::string directory, std::string extension, bool traverse_subdirs,
|
||||
void get_file_names(std::string directory, const std::string & extension, bool traverse_subdirs,
|
||||
string_vector & res);
|
||||
|
||||
bool file_exists(std::string name);
|
||||
bool is_directory(std::string name);
|
||||
bool file_exists(const std::string & name);
|
||||
bool is_directory(const std::string & name);
|
||||
|
||||
std::string get_file_name_without_extension(std::string name);
|
||||
std::string get_file_name_without_extension(const std::string & name);
|
||||
|
||||
// -----------------------------------
|
||||
//
|
||||
|
|
|
|||
|
|
@ -1303,7 +1303,7 @@ private:
|
|||
}
|
||||
}
|
||||
|
||||
void parse_rules_file(std::string fname) {
|
||||
void parse_rules_file(const std::string & fname) {
|
||||
SASSERT(file_exists(fname));
|
||||
flet<std::string> flet_cur_file(m_current_file, fname);
|
||||
|
||||
|
|
@ -1347,7 +1347,7 @@ private:
|
|||
return true;
|
||||
}
|
||||
|
||||
void parse_rel_file(std::string fname) {
|
||||
void parse_rel_file(const std::string & fname) {
|
||||
SASSERT(file_exists(fname));
|
||||
|
||||
IF_VERBOSE(10, verbose_stream() << "Parsing relation file " << fname << "\n";);
|
||||
|
|
@ -1496,7 +1496,7 @@ private:
|
|||
return true;
|
||||
}
|
||||
|
||||
void parse_map_file(std::string fname) {
|
||||
void parse_map_file(const std::string & fname) {
|
||||
SASSERT(file_exists(fname));
|
||||
|
||||
IF_VERBOSE(10, verbose_stream() << "Parsing map file " << fname << "\n";);
|
||||
|
|
|
|||
|
|
@ -32,7 +32,7 @@ namespace datalog {
|
|||
predicates.insert(I->first);
|
||||
}
|
||||
|
||||
// reserve pred id = 0 for initalization purposes
|
||||
// reserve pred id = 0 for initialization purposes
|
||||
unsigned num_preds = (unsigned)predicates.size() + 1;
|
||||
|
||||
// poor's man round-up log2
|
||||
|
|
|
|||
|
|
@ -1924,7 +1924,7 @@ namespace datalog {
|
|||
}
|
||||
}
|
||||
|
||||
void finite_product_relation::extract_table_fact(const relation_fact rf, table_fact & tf) const {
|
||||
void finite_product_relation::extract_table_fact(const relation_fact & rf, table_fact & tf) const {
|
||||
const relation_signature & sig = get_signature();
|
||||
relation_manager & rmgr = get_manager();
|
||||
|
||||
|
|
@ -1940,7 +1940,7 @@ namespace datalog {
|
|||
tf.push_back(0);
|
||||
}
|
||||
|
||||
void finite_product_relation::extract_other_fact(const relation_fact rf, relation_fact & of) const {
|
||||
void finite_product_relation::extract_other_fact(const relation_fact & rf, relation_fact & of) const {
|
||||
of.reset();
|
||||
unsigned o_sz = m_other_sig.size();
|
||||
for(unsigned i=0; i<o_sz; i++) {
|
||||
|
|
|
|||
|
|
@ -281,11 +281,11 @@ namespace datalog {
|
|||
\brief Extract the values of table non-functional columns from the relation fact.
|
||||
The value of the functional column which determines index of the inner relation is undefined.
|
||||
*/
|
||||
void extract_table_fact(const relation_fact rf, table_fact & tf) const;
|
||||
void extract_table_fact(const relation_fact & rf, table_fact & tf) const;
|
||||
/**
|
||||
\brief Extract the values of the inner relation columns from the relation fact.
|
||||
*/
|
||||
void extract_other_fact(const relation_fact rf, relation_fact & of) const;
|
||||
void extract_other_fact(const relation_fact & rf, relation_fact & of) const;
|
||||
|
||||
relation_base * mk_empty_inner();
|
||||
relation_base * mk_full_inner(func_decl* pred);
|
||||
|
|
|
|||
|
|
@ -168,7 +168,7 @@ namespace datalog {
|
|||
}
|
||||
|
||||
|
||||
void instruction::display_indented(execution_context const & _ctx, std::ostream & out, std::string indentation) const {
|
||||
void instruction::display_indented(execution_context const & _ctx, std::ostream & out, const std::string & indentation) const {
|
||||
out << indentation;
|
||||
rel_context const& ctx = _ctx.get_rel_context();
|
||||
display_head_impl(_ctx, out);
|
||||
|
|
@ -190,7 +190,7 @@ namespace datalog {
|
|||
func_decl_ref m_pred;
|
||||
reg_idx m_reg;
|
||||
public:
|
||||
instr_io(bool store, func_decl_ref pred, reg_idx reg)
|
||||
instr_io(bool store, func_decl_ref const& pred, reg_idx reg)
|
||||
: m_store(store), m_pred(pred), m_reg(reg) {}
|
||||
virtual bool perform(execution_context & ctx) {
|
||||
log_verbose(ctx);
|
||||
|
|
@ -348,7 +348,7 @@ namespace datalog {
|
|||
out << "while";
|
||||
print_container(m_controls, out);
|
||||
}
|
||||
virtual void display_body_impl(execution_context const & ctx, std::ostream & out, std::string indentation) const {
|
||||
virtual void display_body_impl(execution_context const & ctx, std::ostream & out, const std::string & indentation) const {
|
||||
m_body->display_indented(ctx, out, indentation+" ");
|
||||
}
|
||||
};
|
||||
|
|
@ -1182,7 +1182,7 @@ namespace datalog {
|
|||
}
|
||||
}
|
||||
|
||||
void instruction_block::display_indented(execution_context const& _ctx, std::ostream & out, std::string indentation) const {
|
||||
void instruction_block::display_indented(execution_context const& _ctx, std::ostream & out, const std::string & indentation) const {
|
||||
rel_context const& ctx = _ctx.get_rel_context();
|
||||
instr_seq_type::const_iterator it = m_data.begin();
|
||||
instr_seq_type::const_iterator end = m_data.end();
|
||||
|
|
|
|||
|
|
@ -150,7 +150,7 @@ namespace datalog {
|
|||
return m_reg_annotation.find(reg, res);
|
||||
}
|
||||
|
||||
void set_register_annotation(reg_idx reg, std::string str) {
|
||||
void set_register_annotation(reg_idx reg, const std::string & str) {
|
||||
m_reg_annotation.insert(reg, str);
|
||||
}
|
||||
|
||||
|
|
@ -233,7 +233,7 @@ namespace datalog {
|
|||
|
||||
Each line must be prepended by \c indentation and ended by a newline character.
|
||||
*/
|
||||
virtual void display_body_impl(execution_context const & ctx, std::ostream & out, std::string indentation) const {}
|
||||
virtual void display_body_impl(execution_context const & ctx, std::ostream & out, const std::string & indentation) const {}
|
||||
void log_verbose(execution_context& ctx);
|
||||
|
||||
public:
|
||||
|
|
@ -249,7 +249,7 @@ namespace datalog {
|
|||
void display(execution_context const& ctx, std::ostream & out) const {
|
||||
display_indented(ctx, out, "");
|
||||
}
|
||||
void display_indented(execution_context const & ctx, std::ostream & out, std::string indentation) const;
|
||||
void display_indented(execution_context const & ctx, std::ostream & out, const std::string & indentation) const;
|
||||
|
||||
static instruction * mk_load(ast_manager & m, func_decl * pred, reg_idx tgt);
|
||||
/**
|
||||
|
|
@ -359,7 +359,7 @@ namespace datalog {
|
|||
void display(execution_context const & ctx, std::ostream & out) const {
|
||||
display_indented(ctx, out, "");
|
||||
}
|
||||
void display_indented(execution_context const & ctx, std::ostream & out, std::string indentation) const;
|
||||
void display_indented(execution_context const & ctx, std::ostream & out, const std::string & indentation) const;
|
||||
|
||||
unsigned num_instructions() const { return m_data.size(); }
|
||||
};
|
||||
|
|
|
|||
|
|
@ -454,7 +454,7 @@ namespace datalog {
|
|||
: m_manager(ctx.get_manager()),
|
||||
m_subst(ctx.get_var_subst()),
|
||||
m_col_idx(col_idx),
|
||||
m_new_rule(new_rule) {}
|
||||
m_new_rule(std::move(new_rule)) {}
|
||||
|
||||
virtual void operator()(relation_base & r0) {
|
||||
explanation_relation & r = static_cast<explanation_relation &>(r0);
|
||||
|
|
|
|||
|
|
@ -488,7 +488,7 @@ namespace datalog {
|
|||
ptr_vector<relation_transformer_fn> m_transforms;
|
||||
public:
|
||||
transform_fn(relation_signature s, unsigned num_trans, relation_transformer_fn** trans):
|
||||
m_sig(s),
|
||||
m_sig(std::move(s)),
|
||||
m_transforms(num_trans, trans) {}
|
||||
|
||||
~transform_fn() { dealloc_ptr_vector_content(m_transforms); }
|
||||
|
|
|
|||
|
|
@ -289,7 +289,7 @@ namespace datalog {
|
|||
relation_transformer_fn * mk_permutation_rename_fn(const relation_base & t,
|
||||
const unsigned * permutation);
|
||||
relation_transformer_fn * mk_permutation_rename_fn(const relation_base & t,
|
||||
const unsigned_vector permutation) {
|
||||
const unsigned_vector & permutation) {
|
||||
SASSERT(t.get_signature().size()==permutation.size());
|
||||
return mk_permutation_rename_fn(t, permutation.c_ptr());
|
||||
}
|
||||
|
|
@ -343,7 +343,7 @@ namespace datalog {
|
|||
|
||||
relation_mutator_fn * mk_filter_identical_fn(const relation_base & t, unsigned col_cnt,
|
||||
const unsigned * identical_cols);
|
||||
relation_mutator_fn * mk_filter_identical_fn(const relation_base & t, const unsigned_vector identical_cols) {
|
||||
relation_mutator_fn * mk_filter_identical_fn(const relation_base & t, const unsigned_vector & identical_cols) {
|
||||
return mk_filter_identical_fn(t, identical_cols.size(), identical_cols.c_ptr());
|
||||
}
|
||||
|
||||
|
|
@ -468,7 +468,7 @@ namespace datalog {
|
|||
of column number.
|
||||
*/
|
||||
table_transformer_fn * mk_permutation_rename_fn(const table_base & t, const unsigned * permutation);
|
||||
table_transformer_fn * mk_permutation_rename_fn(const table_base & t, const unsigned_vector permutation) {
|
||||
table_transformer_fn * mk_permutation_rename_fn(const table_base & t, const unsigned_vector & permutation) {
|
||||
SASSERT(t.get_signature().size()==permutation.size());
|
||||
return mk_permutation_rename_fn(t, permutation.c_ptr());
|
||||
}
|
||||
|
|
@ -522,7 +522,7 @@ namespace datalog {
|
|||
|
||||
table_mutator_fn * mk_filter_identical_fn(const table_base & t, unsigned col_cnt,
|
||||
const unsigned * identical_cols);
|
||||
table_mutator_fn * mk_filter_identical_fn(const table_base & t, const unsigned_vector identical_cols) {
|
||||
table_mutator_fn * mk_filter_identical_fn(const table_base & t, const unsigned_vector & identical_cols) {
|
||||
return mk_filter_identical_fn(t, identical_cols.size(), identical_cols.c_ptr());
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -67,7 +67,7 @@ namespace datalog {
|
|||
}
|
||||
|
||||
relation_base * sieve_relation::complement(func_decl* p) const {
|
||||
//this is not precisely a complement, because we still treat the ignored collumns as
|
||||
//this is not precisely a complement, because we still treat the ignored columns as
|
||||
//full, but it should give reasonable results inside the product relation
|
||||
relation_base * new_inner = get_inner().complement(p);
|
||||
return get_plugin().mk_from_inner(get_signature(), m_inner_cols.c_ptr(), new_inner);
|
||||
|
|
|
|||
|
|
@ -108,7 +108,7 @@ namespace datalog {
|
|||
|
||||
sieve_relation * mk_from_inner(const relation_signature & s, const bool * inner_columns,
|
||||
relation_base * inner_rel);
|
||||
sieve_relation * mk_from_inner(const relation_signature & s, const svector<bool> inner_columns,
|
||||
sieve_relation * mk_from_inner(const relation_signature & s, const svector<bool> & inner_columns,
|
||||
relation_base * inner_rel) {
|
||||
SASSERT(inner_columns.size()==s.size());
|
||||
return mk_from_inner(s, inner_columns.c_ptr(), inner_rel);
|
||||
|
|
|
|||
|
|
@ -424,7 +424,7 @@ namespace datalog {
|
|||
|
||||
/**
|
||||
\c array \c removed_cols contains column indexes to be removed in ascending order and
|
||||
is terminated by a number greated than the highest column index of a join the the two tables.
|
||||
is terminated by a number greater than the highest column index of a join the two tables.
|
||||
This is to simplify the traversal of the array when building facts.
|
||||
*/
|
||||
static void concatenate_rows(const column_layout & layout1, const column_layout & layout2,
|
||||
|
|
@ -436,7 +436,7 @@ namespace datalog {
|
|||
columns from t2 using indexing.
|
||||
|
||||
\c array \c removed_cols contains column indexes to be removed in ascending order and
|
||||
is terminated by a number greated than the highest column index of a join the the two tables.
|
||||
is terminated by a number greater than the highest column index of a join the two tables.
|
||||
This is to simplify the traversal of the array when building facts.
|
||||
|
||||
\c tables_swapped value means that the resulting facts should contain facts from t2 first,
|
||||
|
|
|
|||
|
|
@ -240,7 +240,7 @@ namespace datalog {
|
|||
|
||||
const table_relation & tr_src = static_cast<const table_relation &>(src);
|
||||
relation_manager & rmgr = tr_src.get_manager();
|
||||
relation_signature sig = tr_src.get_signature();
|
||||
const relation_signature & sig = tr_src.get_signature();
|
||||
SASSERT(tgt.get_signature()==sig);
|
||||
SASSERT(!delta || delta->get_signature()==sig);
|
||||
|
||||
|
|
|
|||
|
|
@ -3418,7 +3418,7 @@ expr_ref context::get_constraints (unsigned level)
|
|||
return m_pm.mk_and (constraints);
|
||||
}
|
||||
|
||||
void context::add_constraints (unsigned level, expr_ref c)
|
||||
void context::add_constraints (unsigned level, const expr_ref& c)
|
||||
{
|
||||
if (!c.get()) { return; }
|
||||
if (m.is_true(c)) { return; }
|
||||
|
|
|
|||
|
|
@ -833,7 +833,7 @@ public:
|
|||
pob& get_root() const { return m_pob_queue.get_root(); }
|
||||
|
||||
expr_ref get_constraints (unsigned lvl);
|
||||
void add_constraints (unsigned lvl, expr_ref c);
|
||||
void add_constraints (unsigned lvl, const expr_ref& c);
|
||||
};
|
||||
|
||||
inline bool pred_transformer::use_native_mbp () {return ctx.use_native_mbp ();}
|
||||
|
|
|
|||
|
|
@ -42,7 +42,7 @@ namespace spacer
|
|||
return m_num_cols;
|
||||
}
|
||||
|
||||
rational spacer_matrix::get(unsigned int i, unsigned int j)
|
||||
const rational& spacer_matrix::get(unsigned int i, unsigned int j)
|
||||
{
|
||||
SASSERT(i < m_num_rows);
|
||||
SASSERT(j < m_num_cols);
|
||||
|
|
@ -50,7 +50,7 @@ namespace spacer
|
|||
return m_matrix[i][j];
|
||||
}
|
||||
|
||||
void spacer_matrix::set(unsigned int i, unsigned int j, rational v)
|
||||
void spacer_matrix::set(unsigned int i, unsigned int j, const rational& v)
|
||||
{
|
||||
SASSERT(i < m_num_rows);
|
||||
SASSERT(j < m_num_cols);
|
||||
|
|
|
|||
|
|
@ -25,13 +25,13 @@ namespace spacer {
|
|||
|
||||
class spacer_matrix {
|
||||
public:
|
||||
spacer_matrix(unsigned m, unsigned n); // m rows, n colums
|
||||
spacer_matrix(unsigned m, unsigned n); // m rows, n columns
|
||||
|
||||
unsigned num_rows();
|
||||
unsigned num_cols();
|
||||
|
||||
rational get(unsigned i, unsigned j);
|
||||
void set(unsigned i, unsigned j, rational v);
|
||||
const rational& get(unsigned i, unsigned j);
|
||||
void set(unsigned i, unsigned j, const rational& v);
|
||||
|
||||
unsigned perform_gaussian_elimination();
|
||||
|
||||
|
|
|
|||
|
|
@ -301,7 +301,7 @@ public:
|
|||
void operator()(quantifier*) {}
|
||||
};
|
||||
|
||||
void unsat_core_learner::collect_symbols_b(expr_set axioms_b)
|
||||
void unsat_core_learner::collect_symbols_b(const expr_set& axioms_b)
|
||||
{
|
||||
expr_mark visited;
|
||||
collect_pure_proc proc(m_symbols_b);
|
||||
|
|
|
|||
|
|
@ -82,7 +82,7 @@ namespace spacer {
|
|||
private:
|
||||
ptr_vector<unsat_core_plugin> m_plugins;
|
||||
func_decl_set m_symbols_b; // symbols, which occur in any b-asserted formula
|
||||
void collect_symbols_b(expr_set axioms_b);
|
||||
void collect_symbols_b(const expr_set& axioms_b);
|
||||
|
||||
ast_mark m_a_mark;
|
||||
ast_mark m_b_mark;
|
||||
|
|
|
|||
|
|
@ -242,7 +242,7 @@ namespace nlsat {
|
|||
}
|
||||
|
||||
/**
|
||||
\breif Store in ps the polynomials occurring in the given literals.
|
||||
\brief Store in ps the polynomials occurring in the given literals.
|
||||
*/
|
||||
void collect_polys(unsigned num, literal const * ls, polynomial_ref_vector & ps) {
|
||||
ps.reset();
|
||||
|
|
@ -332,7 +332,7 @@ namespace nlsat {
|
|||
if (!is_zero(lc)) {
|
||||
if (sign(lc) != 0)
|
||||
return;
|
||||
// lc is not the zero polynomial, but it vanished in the current interpretaion.
|
||||
// lc is not the zero polynomial, but it vanished in the current interpretation.
|
||||
// so we keep searching...
|
||||
add_zero_assumption(lc);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1791,7 +1791,7 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
void context::set_conflict(b_justification js, literal not_l) {
|
||||
void context::set_conflict(const b_justification & js, literal not_l) {
|
||||
if (!inconsistent()) {
|
||||
TRACE("set_conflict", display_literal_verbose(tout, not_l); display(tout, js); );
|
||||
m_conflict = js;
|
||||
|
|
|
|||
|
|
@ -897,7 +897,7 @@ namespace smt {
|
|||
void trace_assign(literal l, b_justification j, bool decision) const;
|
||||
|
||||
public:
|
||||
void assign(literal l, b_justification j, bool decision = false) {
|
||||
void assign(literal l, const b_justification & j, bool decision = false) {
|
||||
SASSERT(l != false_literal);
|
||||
SASSERT(l != null_literal);
|
||||
switch (get_assignment(l)) {
|
||||
|
|
@ -998,9 +998,9 @@ namespace smt {
|
|||
|
||||
void assign_quantifier(quantifier * q);
|
||||
|
||||
void set_conflict(b_justification js, literal not_l);
|
||||
void set_conflict(const b_justification & js, literal not_l);
|
||||
|
||||
void set_conflict(b_justification js) {
|
||||
void set_conflict(const b_justification & js) {
|
||||
set_conflict(js, null_literal);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -387,9 +387,9 @@ static void tst9() {
|
|||
|
||||
static void tst10(bool use_ints) {
|
||||
if (use_ints)
|
||||
std::cout << "Testing multiplication performace using small ints\n";
|
||||
std::cout << "Testing multiplication performance using small ints\n";
|
||||
else
|
||||
std::cout << "Testing multiplication performace using small rationals\n";
|
||||
std::cout << "Testing multiplication performance using small rationals\n";
|
||||
vector<rational> vals;
|
||||
vector<rational> vals2;
|
||||
vector<float> fvals;
|
||||
|
|
|
|||
|
|
@ -47,7 +47,7 @@ public:
|
|||
set_global_param('pp.decimal', 'true')
|
||||
will set the parameter "decimal" in the module "pp" to true.
|
||||
|
||||
An exception is thrown if the the parameter name is unknown, or if the value is incorrect.
|
||||
An exception is thrown if the parameter name is unknown, or if the value is incorrect.
|
||||
*/
|
||||
static void set(char const * name, char const * value);
|
||||
static void set(symbol const & name, char const * value);
|
||||
|
|
@ -57,7 +57,7 @@ public:
|
|||
|
||||
If the parameter is not set, then it just returns 'default'.
|
||||
|
||||
An exception is thrown if the the parameter name is unknown.
|
||||
An exception is thrown if the parameter name is unknown.
|
||||
*/
|
||||
static std::string get_value(char const * name);
|
||||
static std::string get_value(symbol const & name);
|
||||
|
|
|
|||
|
|
@ -187,7 +187,7 @@ class mpz_manager {
|
|||
|
||||
/**
|
||||
\brief Set \c a with the value stored at m_tmp[IDX], and the given sign.
|
||||
\c sz is an overapproximation of the the size of the number stored at \c tmp.
|
||||
\c sz is an overapproximation of the size of the number stored at \c tmp.
|
||||
*/
|
||||
template<int IDX>
|
||||
void set(mpz & a, int sign, unsigned sz);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue