mirror of
https://github.com/Z3Prover/z3
synced 2025-11-03 21:09:11 +00:00
70 lines
1.5 KiB
C++
70 lines
1.5 KiB
C++
/*++
|
|
Copyright (c) 2012 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
goal2nlsat.h
|
|
|
|
Abstract:
|
|
|
|
"Compile" a goal into the nonlinear arithmetic engine.
|
|
Non-arithmetic atoms are "abstracted" into boolean variables.
|
|
Non-supported terms are "abstracted" into variables.
|
|
|
|
The mappings can be used to convert back the state of the
|
|
engine into a goal.
|
|
|
|
Author:
|
|
|
|
Leonardo (leonardo) 2012-01-02
|
|
|
|
Notes:
|
|
|
|
--*/
|
|
#pragma once
|
|
|
|
#include "nlsat/nlsat_types.h"
|
|
#include "tactic/model_converter.h"
|
|
|
|
class goal;
|
|
class expr2var;
|
|
|
|
class goal2nlsat {
|
|
struct imp;
|
|
imp * m_imp;
|
|
struct scoped_set_imp;
|
|
public:
|
|
goal2nlsat();
|
|
~goal2nlsat();
|
|
|
|
static void collect_param_descrs(param_descrs & r);
|
|
|
|
/**
|
|
\brief "Compile" the goal into the given nlsat engine.
|
|
Store a mapping from atoms to boolean variables into a2b.
|
|
Store a mapping from terms into arithmetic variables into t2x.
|
|
|
|
\remark a2b and t2x m don't need to be empty. The definitions there are reused.
|
|
|
|
The input is expected to be in CNF
|
|
*/
|
|
void operator()(goal const & g, params_ref const & p, nlsat::solver & s, expr2var & a2b, expr2var & t2x);
|
|
|
|
};
|
|
|
|
class nlsat2goal {
|
|
struct imp;
|
|
imp * m_imp;
|
|
public:
|
|
nlsat2goal(ast_manager& m);
|
|
~nlsat2goal();
|
|
|
|
static void collect_param_descrs(param_descrs & r);
|
|
|
|
/**
|
|
\brief Translate a literal into a formula.
|
|
*/
|
|
expr_ref operator()(nlsat::solver& s, u_map<expr*> const& b2a, u_map<expr*> const& x2t, nlsat::literal l);
|
|
|
|
};
|
|
|